London Mathematical Society, LMS Journal of Computation and Mathematics, (6), p. 198-248, 2003
DOI: 10.1112/s1461157000000449
Logic and Theory of Algorithms, p. 486-490
DOI: 10.1007/978-3-540-69407-6_52
Full text: Download
AbstractThe proof of the relative consistency of the axiom of choice has been mechanized using Isabelle⁄ZF, building on a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the formalization unusually long, and not entirely satisfactory: two parts of the proof do not fit together. It seems impossible to solve these problems without formalizing the metatheory. However, the present development follows a standard textbook, Kenneth Kunen's Set theory: an introduction to independence proofs, and could support the formalization of further material from that book. It also serves as an example of what to expect when deep mathematics is formalized.