Teaching a Formalized Logical Calculus

Andreas Halkjær From, Alexander Birch Jensen, Anders Schlichtkrull, Jørgen Villadsen*

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

142 Downloads (Pure)


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
Pages (from-to)73-92
Publication statusPublished - 2020
Event8th International Workshop on Theorem Proving Components for Educational Software - Praiamar Hotel, Natal, Brazil
Duration: 25 Aug 201925 Aug 2019
Conference number: 8


Workshop8th International Workshop on Theorem Proving Components for Educational Software
LocationPraiamar Hotel
Internet address


Dive into the research topics of 'Teaching a Formalized Logical Calculus'. Together they form a unique fingerprint.

Cite this