The relative consistency of the axiom of choice mechanized using Isabelle/ZF
Lawrence C. Paulson
Abstract: The 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.
|
