Felix Rech: Master’s Thesis

Saarland University Computer Science

Mechanising Set Theory in Coq

The Generalised Continuum Hypothesis and the Axiom of Choice

Advisor: Dominik Kirst

I started from a second-order axiomatisation of Zermelo-Fraenkel set theory (ZF) in the Coq proof assistant and formalised a proof of Sierpiński’s theorem [1] which states that the generalised continuum hypothesis implies the axiom of choice.

During the second part of my project, I worked towards a formal proof of the relative consistency of the generalised continuum hypothesis and the axiom of choice over first-order ZF [2]. The proof relies on the constructible universe as a model that satisfies both hypotheses.

In order to make the formulation of complex statements in first-order logic feasible, I developed a compositional reification framework. The framework can handle statements from a large fragment of Coq including higher-order functions, dependent types and quantification over things that can be encoded as sets. In many cases, the reification can happen implicitly. This allows us to use many set-theoretic notations in the same way as in informal mathematics.


  1. Wacław Sierpiński.
    L’hypothèse généralisée du continu et l’axiome du choix.
    In: Fundamenta Mathematicae 1.34 (1947), pp. 1–5.
  2. Kurt Gödel.
    The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis.
    In: Proceedings of the National Academy of Sciences of the United States of America 24.12 (1938), p. 556.


Legal notice, Privacy policy