Felix Rech: Master’s Thesis

Saarland University Computer Science

On the Generalized Continuum Hypothesis in Coq

Advisor: Dominik Kirst


The generalized continuum hypothesis in Zermelo-Fraenkel set theory states that no cardinality lies strictly between that of any infinite set and its power set. The axiom of choice states that for every set A of nonempty sets, there is a choice function that maps every B ∈ A to an element of B. Both are independent of the Zermelo-Fraenkel axioms but Sierpiński’s theorem states that the generalized continuum hypothesis implies the axiom of choice [1].

I translated this result into a second-order axiomatization of Zermelo-Fraenkel set theory and formalized it in the Coq proof assistant. Possible future goals are the construction of a model that satisfies the general continuum hypothesis and a proof of a type theoretic version of the theorem.



  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.

Legal notice, Privacy policy