Mechanizing Set Theory Using Isabelle
Axiomatic set theory is the foundation of mathematics, but for most people it is obscure and incomprehensible. The papers described below concern Isabelle/ZF, which provides an interactive environment for undertaking set theory proofs.
Isabelle's architecture, based on a logical framework, allows it to support ZF set theory within the context of first-order logic.
The highlight of this work is the formalisation of Gödel's
constructible universe, a feat that cannot even be attempted using most verification tools.
- L. C. Paulson.
Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389.
- L. C. Paulson.
A fixedpoint approach to implementing (co)inductive definitions (revised version). In: A. Bundy (editor), 12th International Conf. on Automated Deduction (Springer LNAI 814, 1994), 148–161.
Slides available
- L. C. Paulson.
Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
- L. C. Paulson.
Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. (With Krzysztof Grabczewski.)
Slides available
- L. C. Paulson.
Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
- L. C. Paulson.
The reflection theorem: a study in meta-theoretic reasoning.
In: A. Voronkov (editor), 18th International Conf. on Automated Deduction: CADE-18 (Springer LNAI 2392, 2002), 377–391.
Slides available
- L. C. Paulson.
The relative consistency of the axiom of choice — mechanized using Isabelle/ZF.
LMS J. Computation and Mathematics 6 (2003), 198–248.
Slides and theory document available