Department of Computer Science and Technology

Technical reports

Mechanising set theory: cardinal arithmetic and the axiom of choice

Larry Paulson, Krzysztof Grabczewski

July 1995, 33 pages


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.

Full text

PDF (0.3 MB)
PS (0.1 MB)

BibTeX record

  author =	 {Paulson, Larry and Grabczewski, Krzysztof},
  title = 	 {{Mechanising set theory: cardinal arithmetic and the axiom
         	   of choice}},
  year = 	 1995,
  month = 	 jul,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-377}