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.