Metamathematics, machines and Gödel's proof presents a computerized proof of Gödel's incompleteness theorem itself. The author uses the lisp programming language, firstly to write a program to check proofs for the first order set-theoretic language Z2, and secondly to express the proof checking program itself in Z2, using the Boyer-Moore theorem prover to prove the existence of an unprovable sentence

I wouldn't, however, recommend this book to the novice - its more for those with some experience of computer-based proofs, or possibly for those interested in what can be done with the lisp language. Even for those familiar with arithmetical proofs, the connection with the programs in the book isn't immediately clear, especially as it uses Z2 rather than Peano Arithmetic. But the more advanced approach does result in a more reliable form of proof than might otherwise be the case - a true computer based proof, rather than just using a computer to help persuade someone of the truth of a theorem."; include "amazinf.php"; ?>