RICHARDSON@SU-SCORE.ARPA (Anne Richardson) (05/08/86)
Natarajan Shankar will be visiting CSD on Thursday, May 15. While here, he
will be giving the following talk:
DAY: May 15, 1986
EVENT: AI Seminar
PLACE: Bldg. 380, Room 380 X
TIME: 5:15
TITLE: Checking the Proof of Godel's Incompleteness Theorem
with the Boyer-Moore theorem prover.
PERSON: Natarajan Shankar
FROM: The University of Texas at Austin
There is a widespread belief that computer proof-checking of significant
proofs in mathematics is infeasible. We argue against this belief by
presenting a formalization and proof of Godel's incompleteness theorem
that was checked with the Boyer-Moore theorem prover. This mechanical
proof establishes the essential incompleteness of Cohen's Z2 axioms for
hereditarily finite sets. The proof involves a metatheoretic formalization
of Shoenfield's first-order logic along with Cohen's Z2 axioms. Several
derived inference rules were proved as theorems about this logic. These
derived inference rules were used to develop enough set theory in order
to demonstrate the representability of a Lisp interpreter in this logic.
The Lisp interpreter was used to establish the computability of the
metatheoretic formalization of Z2. From this, the representability of
the Lisp interpreter, and the enumerability of proofs, an undecidable
sentence was constructed. The theorem prover was led to the observation
that if the undecidable sentence is either provable or disprovable, then
it is both provable and disprovable. The theory is therefore either
incomplete or inconsistent.