Abstract
We show how codatatypes can be employed to produce compact, high-level proofs of key results in logic: the soundness and completeness of proof systems for variations of first-order logic. For the classical completeness result, we first establish an abstract property of possibly infinite derivation trees. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems for various flavors of first-order logic. Soundness becomes interesting as soon as one allows infinite proofs of first-order formulas. This forms the subject of several cyclic proof systems for first-order logic augmented with inductive predicate definitions studied in the literature. All the discussed results are formalized using Isabelle/HOL’s recently introduced support for codatatypes and corecursion. The development illustrates some unique features of Isabelle/HOL’s new coinductive specification language such as nesting through non-free types and mixed recursion–corecursion.
Original language | English |
---|---|
Pages (from-to) | 149-179 |
Number of pages | 31 |
Journal | Journal of Automated Reasoning |
Volume | 58 |
Issue number | 1 |
DOIs | |
Publication status | Published - Jan 2017 |
Keywords
- Codatatypes
- Completeness
- First-order logic
- Gentian systems
- Isabelle/HOL
- Lazy evaluation
- Proof assistants
- Soundness