roseh@RATLIFF.UTEXAS.EDU (Rose M. Herring) (02/28/86)
University of Texas
Computer Sciences Department
COLLOQUIUM
SPEAKER: N. Shankar
University of Texas at Austin
TITLE: Checking the Proof of Godel's Incompleteness
Theorem with the Boyer-Moore Theorem Prover
DATE: Thursday, March 6, 1986
PLACE: WEL 3.502
TIME: 4:00-5:30 p.m.
There is a widespread belief that computer proof-checking
of significant mathematics is infeasible. We argue against this
by presenting a machine-checked proof of Godel's incompleteness
theorem, one of the greatest landmarks of mathematics. The proof
of this theorem was checked in a constructive logic with the
Boyer-Moore theorem prover. The proof demonstrates the essential
incompleteness of Cohen's axioms for hereditarily finite sets.
This was done by first formalizing a proof-checker for this log-
ic, extending it with derived inference rules, demonstrating the
representability of a Lisp Eval function by a predicate in this
logic, and then constructing an undecidable sentence. The state-
ment of the incompleteness theorem as proved, asserts that if the
undecidable sentence is either provable or disprovable, then it
is both provable and disprovable. This shows that the above ax-
iom system is either incomplete or inconsistent.