Mechanizing Set Theory

Cardinal Arithmetic and the Axiom of Choice

Lawrence C. Paulson
Computer Laboratory, University of Cambridge
email: [email protected]

Krzysztof Grabczewski
Nicholas Copernicus University, Toru?n, Poland
email: [email protected]

(Received ..... ; Accepted in final form .....)

Abstract. 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 <= ? <= = <=, where <= 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.

Key words: Isabelle, cardinal arithmetic, Axiom of Choice, set theory, QED project