Proof-Checking Metamathematics

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.