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.