| Home |
| About |
| Submission Guidelines |
| Updating entries |
| Search |
| Index |
| Download |
project summary
Completeness theorem
| Title: | Completeness theorem |
| Author: | James Margetson and Tom Ridge |
| Submission date: | 2004-09-20 |
| 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]. |
| BibTeX: |
@article{Completeness-AFP,
author = {James Margetson and Tom Ridge},
title = {Completeness theorem},
journal = {Archive of Formal Proofs},
month = sep,
year = 2004,
note = {\url{http://afp.sf.net/entries/Completeness},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Status: [ok] | This is the development version, revision 9ce4a76615bb, of this entry, generated for Isabelle revision 0e70511cbba9. The development version might change over time and is only permanently archived at Isabelle release points. It is provided as a preview of the next upcoming release. Please refer to release versions only in citations. If the status shows [FAIL], the links below will point to the last working version if any. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|