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 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
Continued..
|
|
|