Logical Approaches to Computational Barriers

The relative consistency of the axiom of choice mechanized using Isabelle/ZF

Speaker:
| Lawrence C Paulson |

Gödel's 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, which would make the proof quite
different from Gödel's. 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.

websites: Arnold Beckmann | 2008-05-23 |