Teaching a Formalized Logical Calculus

TL;DR

This paper formalizes a sequent calculus for first-order logic in Isabelle/HOL, proving soundness and completeness, and discusses the methodology and educational use of the formalization.

Contribution

It provides a detailed formalization of first-order logic sequent calculus in Isabelle/HOL, including proofs of soundness and completeness, using de Bruijn indices and a programming-like approach.

Findings

Formalization of sequent calculus in Isabelle/HOL

Proofs of soundness and completeness established

Educational application in a logic course

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.