Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Wed, 26 Jul 1995 17:16:54 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id LAA24786 for qed-out; Wed, 26 Jul 1995 11:09:43 -0500 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id LAA24780 for ; Wed, 26 Jul 1995 11:09:28 -0500 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 26 Jul 1995 17:07:22 +0100 X-Mailer: exmh version 1.6.1 5/23/95 To: bra-types@cs.chalmers.se, logic@cs.cornell.edu, info-hol@leopard.cs.byu.edu, theorem-provers@mc.lcs.mit.edu, qed@mcs.anl.gov cc: Krzysztof Grabczewski Subject: paper available X-uri: X-face: "OrDM]eXxWpb;,!g'n)u!-ss/8qvWB4*r>rA5~IAaMPwt$YO^oBckRP3N&D0.K"wKN7B> E&BJ5P-gy=o">rX=;.8M:sNp55m9?O%dK#v4{5e#8=-q9FUHURBbRfE:g\DybYQW4~MkQ 13swsz`i*9}*8fy}.au9jo. Date: Wed, 26 Jul 1995 17:07:12 +0100 From: Lawrence C Paulson Message-ID: <"swan.cl.cam.:236820:950726160737"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk The paper described below is available on the WWW via the URL 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.