# Interactively explorable formal proofs for textbooks of mathematics

 dc.contributor Aalto-yliopisto fi dc.contributor Aalto University en dc.contributor.advisor Janhunen, Tomi dc.contributor.author Peltola, Veli dc.date.accessioned 2015-10-16T08:51:55Z dc.date.available 2015-10-16T08:51:55Z dc.date.issued 2015-09-29 dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/18170 dc.description.abstract Electronic textbooks of mathematics would benefit from interactively explorable proofs, where the reader can request a more detailed explanation for any part of the proof he or she does not understand. This requires that definitions, theorem statements, and proofs are written in some formal language. In this thesis we investigate the theoretical and practical challenges of producing such textbooks. en Any particular choice of language cannot be adequate for all textbooks, so we construct a theoretical framework for discussing extensible languages. Under this framework we define three languages for expressing definitions and theorem statements. The first two correspond to the standard languages of propositional and first-order logics. The third language is expressive enough for most definitions and theorem statements in discrete mathematics, but conceptually less problematic than the languages of set theory and higher-order logic, because it cannot express unrestricted quantification over sets that are larger than the set of real numbers. In addition, an implementation of an interactive proof explorer is presented. Its capabilities are demonstrated with an explorable proof of Bertrand’s postulate. The focus of this thesis is on the experience of the reader, and the results seem promising in that regard. With further work on making the authoring tools more efficient to use, it should be feasible to formalize an entire textbook. dc.description.abstract Sähköisissä matematiikan oppikirjoissa olisi hyötyä interaktiivisista todistuksista, joiden avulla lukija voisi pyytää tarkentavaa selitystä mihin tahansa kohtaan, jota hän ei ymmärrä. Tällaisen kirjan kirjoittaminen vaatii, että määritelmät, lauseet ja todistukset on kirjoitettu jollain formaalilla kielellä. Tässä diplomityössä tutkitaan sekä käytännön että teorian tasolla interaktiivisia todistuksia sisältävien oppikirjojen kirjoittamiseen liittyviä haasteita. fi Koska mikään yksittäinen kieli ei voi olla riittävä kaikkien oppikirjojen tarpeisiin, työssä määritellään kielen laajentamisen käsite. Tämän viitekehyksen sisällä kehitetään määritelmille ja lauseille kolme kieltä, joista kaksi ensimmäistä vastaavat lauselogiikkaa ja ensimmäisen kertaluvun predikaattilogiikkaa. Kolmas kieli, joka on näiden laajennus, on ilmaisuvoimaltaan riittävä monien diskreettiin matematiikkaan keskittyvien oppikirjojen formalisoimiseen. Tämä kieli on käsitteellisesti yksinkertaisempi kuin joukko-opin tai korkeamman kertaluvun predikaattilogiikan kielet, koska siinä ei pysty rajoittamattomasti kvantifioimaan sellaisten joukkojen yli, jotka ovat suurempia kuin reaalilukujen joukko. Lisäksi työssä esitellään tietokoneohjelma, jonka avulla interaktiivisesti tarkasteltavia formaaleja todistuksia voi lukea, sekä tämän ohjelman avulla kirjoitettu Bertrandin postulaatin todistus. Tässä työssä keskitytään todistuksiin lukijan näkökulmasta, ja tulokset ovat siltä osin lupaavia. Kokonaisen oppikirjan formalisoimiseksi vaaditaan vielä lisätyötä oppikirjan kirjoittajan työn helpottamiseksi. dc.format.extent 73 + 6 dc.format.mimetype application/pdf en dc.language.iso en en dc.title Interactively explorable formal proofs for textbooks of mathematics en dc.title Formaalien todistusten interaktiivinen tarkastelu matematiikan oppikirjoissa fi dc.type G2 Pro gradu, diplomityö en dc.contributor.school Perustieteiden korkeakoulu fi dc.subject.keyword formal languages en dc.subject.keyword formal proofs en dc.subject.keyword mathematics education en dc.subject.keyword first-order logic en dc.subject.keyword second-order arithmetic en dc.subject.keyword continuum hypothesis en dc.identifier.urn URN:NBN:fi:aalto-201510164760 dc.programme.major Matematiikka fi dc.programme.mcode F3006 fi dc.type.ontasot Master's thesis en dc.type.ontasot Diplomityö fi dc.contributor.supervisor Hollanti, Camilla dc.programme Teknillisen fysiikan ja matematiikan koulutusohjelma fi
﻿