Soundness and Completeness Proofs by Coinductive Methods

Jasmin Christian Blanchette, Andrei Popescu, Dmitriy Traytel

Research output: Contribution to JournalArticleAcademicpeer-review

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 languageEnglish
Pages (from-to)149-179
Number of pages31
JournalJournal of Automated Reasoning
Volume58
Issue number1
DOIs
Publication statusPublished - Jan 2017

Keywords

  • Codatatypes
  • Completeness
  • First-order logic
  • Gentian systems
  • Isabelle/HOL
  • Lazy evaluation
  • Proof assistants
  • Soundness

Cite this