Teaching a Formalized Logical Calculus

Research output: Contribution to journalJournal articleResearchpeer-review

32 Downloads (Pure)

Abstract

Classical first-order logic is in many ways central to work in mathematics, linguistics, computer science and artificial intelligence, so it is worthwhile to define it in full detail. We present soundness and completeness proofs of a sequent calculus for first-order logic, formalized in the interactive proof assistant Isabelle/HOL. Our formalization is based on work by Stefan Berghofer, which we have since updated to use Isabelle’s declarative proof style Isar (Archive of Formal Proofs, Entry FOL-Fitting, August 2007 / July 2018). We represent variables with de Bruijn indices; this makes substitution
under quantifiers less intuitive for a human reader. However, the nature of natural numbers yields an elegant solution when compared to implementations of substitution using variables represented by strings. The sequent calculus considered has the special property of an always empty antecedent and a list of formulas in the succedent. We obtain the proofs of soundness and completeness for the sequent calculus as a derived result of the inverse duality of its tableau counterpart. We strive to not only present the results of the proofs of soundness and completeness, but also to provide a deep dive
into a programming-like approach to the formalization of first-order logic syntax, semantics and the sequent calculus. We use the formalization in a bachelor course on logic for computer science and discuss our experiences.
Original languageEnglish
JournalElectronic Proceedings in Theoretical Computer Science
Volume313
Pages (from-to)73-92
ISSN2075-2180
DOIs
Publication statusPublished - 2020
Event8th International Workshop on Theorem Proving Components for Educational Software - Praiamar Hotel, Natal, Brazil
Duration: 25 Aug 201925 Aug 2019
https://www.uc.pt/en/congressos/thedu/thedu19

Conference

Conference8th International Workshop on Theorem Proving Components for Educational Software
LocationPraiamar Hotel
CountryBrazil
CityNatal
Period25/08/201925/08/2019
Internet address

Cite this