practical Proof Checking

Lawrence C Paulson (
Tue, 19 Mar 1996 15:49:51 +0100

> 2) How much are formal proofs longer than usual proofs?

The following paper is relevant. It describes a number of proofs from set
theory, describing their mechanization in Isabelle/ZF and discussing the
relationship between the informal text and the machine proofs.

The short answer is that the expansion factor is quite unpredictable and can
be large (as one might expect).

							Larry Paulson

Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice Lawrence Paulson and Krzysztof Grabczewski

Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanized using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is $\kappa\otimes\kappa=\kappa$, where $\kappa$ is any infinite cardinal. Proving this result required developing theories of orders, order-isomorphisms, order types, ordinal arithmetic, cardinals, etc.; this covers most of Kunen, "Set Theory", Chapter I. Furthermore, we have proved the equivalence of 7 formulations of the Well-ordering Theorem and 20 formulations of AC; this covers the first two chapters of Rubin and Rubin, "Equivalents of the Axiom of Choice", and involves highly technical material. The definitions used in the proofs are largely faithful in style to the original mathematics.

It is on the Web at