Mechanizing Set Theory Using IsabelleIsabelle/ZF logo

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.

  1. L. C. Paulson.
    Set theory for verification: I. From foundations to functions. J. Automated Reasoning 11 (1993), 353–389.
  2. 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
  3. L. C. Paulson.
    Set theory for verification: II. Induction and recursion. J. Automated Reasoning 15 (1995), 167–215.
  4. L. C. Paulson and Krzysztof Grabczewski.
    Mechanizing set theory: cardinal arithmetic and the axiom of choice. J. Automated Reasoning 17 (1996), 291–323. Slides available
  5. L. C. Paulson.
    Final coalgebras as greatest fixed points in ZF set theory. Mathematical Structures in Computer Science 9 (1999), 545–567.
  6. 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. Publisher's version • Slides available
  7. 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
Last revised: 4 April, 2013
Lawrence C. Paulson • Computer Laboratory • University of Cambridge