Formalising Mathematics Using IsabelleIsabelle/ZF logo

Gödel’s Incompleteness Theorems

Gödel’s Incompleteness Theorems are among the most celebrated (and misunderstood) results in mathematics. The first incompleteness theorem states that every sufficiently strong formal theory has an undecidable sentence; the second incompleteness theorem states that no such formal system can prove a theorem that is logically equivalent to its own consistency. While the first theorem has been mechanised using a number of proof assistants as early as 1986, the second incompleteness theorem has never been mechanised until now. The two papers below describe the work (1) for logicians and (2) for researchers in automated reasoning. Slides are also available.

  1. L. C. Paulson.
    A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets. Review of Symbolic Logic (in press). Publisher's version at journals.cambridge.org
  2. L. C. Paulson.
    A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle
    (under review)

Formalising Set Theory

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 versionSlides 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: 9 April, 2014
Lawrence C. PaulsonComputer LaboratoryUniversity of Cambridge