Browse Theses

Formal proof-checking has long been recognized as an interesting application of computers. It has often been claimed that significant proofs in mathematics cannot be checked using an automatic proof-checker, and that formal proofs lack the intuitive plausibility and insight that informal proofs possess. We argue against these claims by presenting machine-checked versions of some landmark proofs in metamathematics, such as those of the tautology theorem, Godel's incompleteness theorem, and the Church-Rosser theorem. These proofs were checked using the Boyer-Moore theorem power.

The tautology theorem and the incompleteness theorem are proved by first defining a proof-checker for the formal theory Z2 in the Boyer-Moore logic. The theory Z2 consists of the rules and axioms for Shoenfield's first-order logic with the axioms of a theory of hereditarily finite sets due to Cohen. A tautology-checker is defined for Z2 formulas and is shown to be correct with respect to the truth-table definition of a tautology. Every tautology is shown to have a proof by defining a Lisp function which constructs such a proof. The tautology theorem is then used as a sound derived inference rule to demonstrate that any specific tautology is provable in Z2, without actually constructing the corresponding formal proof.

To prove Godel's incompleteness theorem, a Lisp interpreter is defined in Lisp. The interpreter is shown to be representable in Z2 under an encoding of Lisp data-structures as sets. Metatheoretic functions such as the Z2 proof-checker are shown to be computable by means of the Lisp interpreter. The representability of the metatheory of Z2 in Z2 permits the construction of an undecidable sentence. If the undecidable sentence is either provable or disprovable, then it is shown to be both provable and disprovable. Z2 is therefore either incomplete or inconsistent.

The mechanical proof of the Church-Rosser theorem is carried out by formalizing the syntax of lambda calculus in the Boyer-Moore logic. The theorem asserts that if the term X is reduced to Y in one way, and Z in another, then Y and Z can both be reduced to a common W. The mechanical proof involves constructing the term W and the reductions from Y and Z to W. This proof was actually carried out by formally mapping the problem to a formalization of lambda calculus which uses the de Bruijn representation. A version of the Tait/Martin-Lof proof of the Church-Rosser theorem is then carried out for this representation.