Metamathematics, machines, and Godel's proof
N Shankar  Cambridge University Press, 1994  ISBN: 052142027X

How much computers can be used to prove mathematical theorems is a question of great interest. Some would claims that Gödel's incompleteness theorem means that there are severe limits on what a computer can do. Well, Metamathematics, machines and Gödel's proof presents a computerized proof of Gödel's incompleteness theorem itself. Natarajan Shankar uses the lisp programming language, firstly to write a program to check proofs for the first order settheoretic language Z2, and secondly to express the proof checking program itself in Z2, using the BoyerMoore theorem prover to prove the existence of an unprovable sentence
Continued..


