The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF

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

• Type: Conference
• Year: 2008
• Where: CIE
• Authors: Lawrence C. Paulson
• Keywords: Applied Computing, CIE 2008, Original Proof, Reflection Theorem, Relative Consistency