Completeness theorem

James Margetson and Tom Ridge

September 20, 2004

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

Abstract

The completeness of first-order logic is proved, following the first five pages of Wainer and Wallen's chapter of the book Proof Theory by Aczel et al., CUP, 1992. Their presentation of formulas allows the proofs to use symmetry arguments. Margetson formalized this theorem by early 2000. The Isar conversion is thanks to Tom Ridge. A paper describing the formalization is available [pdf].

License

BSD License

Topics

Session Completeness

Cite

× 
@article{Completeness-AFP,
  author  = {James Margetson and Tom Ridge},
  title   = {Completeness theorem},
  journal = {Archive of Formal Proofs},
  month   = {September},
  year    = {2004},
  note    = {\url{https://isa-afp.org/entries/Completeness.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest

Older releases: