| Home |
| About |
| Submission Guidelines |
| Search |
| Download |
project summary
Completeness theorem
| Title: | Completeness theorem |
| Author: | James Margetson; ported to Isar by 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]. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|