http://www.cl.cam.ac.uk/users/lcp/ml-aftp/AC.ps.gz
I'm sorry if you get multiple copies of this message.
Lawrence C Paulson, University Lecturer
Computer Laboratory, University of Cambridge,
Pembroke Street, Cambridge CB2 3QG, England
Tel: +44(0)1223 334623 Fax: +44(0)1223 334678
Mechanising Set Theory: Cardinal Arithmetic and the Axiom of Choice
Lawrence C. Paulson & Krzysztof Grabczewski
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.