## Mechanising Set Theory: Cardinal Arithmetic and the Axiom of Choice

*Lawrence C. Paulson*, University of Cambridge, England

*Krzysztof Grąbczewski*, Nicholas Copernicus University, Poland
Fairly deep results of Zermelo-Fraenkel (ZF) set theory have been mechanised using the proof assistant Isabelle. The results concern cardinal arithmetic and the Axiom of Choice (AC). A key result about cardinal multiplication is K*K=K, where K 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*. The definitions used in the proofs are largely faithful in style to the original mathematics.