# Formalising Mathematics Using Isabelle

## 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. The proof scripts and slides are also available.

- 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 - 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.

- 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 and Krzysztof Grabczewski.

Mechanizing set theory: cardinal arithmetic and the axiom of choice.*J. Automated Reasoning***17**(1996), 291–323. 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. Publisher's version • 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

## Miscellaneous Papers

- J. Fleuriot and L. C. Paulson.
Proving Newton's

*Propositio Kepleriana*Using Geometry and Nonstandard Analysis in Isabelle*.*Xiao-Shan Gao, Dongming Wang and Lu Yang (editors),*In*:*Automated Deduction in Geometry, Second International Workshop, ADG '98* - F. Kammüller and L. C. Paulson.
A formal proof of Sylow's theorem: An experiment in abstract algebra with Isabelle HOL.

*J. Automated Reasoning***23**(1999), 235–264. - L. C. Paulson.

Organizing Numerical Theories Using Axiomatic Type Classes.*Journal of Automated Reasoning***33**1 (2004), 29–49.*Slides available* - L. C. Paulson.

Defining Functions on Equivalence Classes.*ACM Trans. on Computational Logic***7**4 (2006), 658–675.*Slides available*