### Abstract

A formalization of an abstract property of possibly infinite derivation trees (modeled by a codatatype), representing the core of a proof (in Beth/Hintikka style) of the first-order logic completeness theorem, independent of the concrete syntax or inference rules. This work is described in detail in the IJCAR 2014 publication by the authors. The abstract proof can be instantiated for a wide range of Gentzen and tableau systems as well as various flavors of FOL---e.g., with or without predicates, equality, or sorts. Here, we give only a toy example instantiation with classical propositional logic. A more serious instance---many-sorted FOL with equality---is described elsewhere [Blanchette and Popescu, FroCoS 2013].

### License

BSD License

### Topics

- Logic/Proof theory

### Session Abstract_Completeness

- Abstract_Completeness
- Propositional_Logic

### Depends on

- Collections Framework

### Used by

- A Naive Prover for First-Order Logic
- A Sequent Calculus Prover for First-Order Logic with Functions
- Abstract Soundness
- The meta theory of the Incredible Proof Machine

### Auto-related entries

- Suppes' Theorem For Probability Logic
- Propositional Proof Systems

## Cite

×

Abstract_Completeness-AFP

    @article{Abstract_Completeness-AFP,
      author  = {Jasmin Christian Blanchette and Andrei Popescu and Dmitriy Traytel},
      title   = {Abstract Completeness},
      journal = {Archive of Formal Proofs},
      month   = {April},
      year    = {2014},
      note    = {\url{https://isa-afp.org/entries/Abstract_Completeness.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Apr 16, 2014 : Isabelle2013-2