## Completeness theorem

swMATH ID: | 28562 |

Software Authors: | James Margetson; Tom Ridge |

Description: | Completeness theorem: 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. |

Homepage: | https://www.isa-afp.org/entries/Completeness.html |

Dependencies: | Isabelle |

Related Software: | Archive Formal Proofs; Isabelle/HOL; FOL Fitting; HOL; Sledgehammer; Isabelle; Isar; Abstract Completeness; IsaFoL; FOL_Harrison; Verified Prover; Superposition Calculus; GitHub; Jitawa; Milawa; LCF; SPASS; ML; HOL Light; Metamath |

Referenced in: | 8 Publications |

all
top 5

### Referenced by 19 Authors

### Referenced in 2 Serials

5 | Journal of Automated Reasoning |

1 | AI Communications |

### Referenced in 2 Fields

8 | Computer science (68-XX) |

5 | Mathematical logic and foundations (03-XX) |