Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq

Dominik Kirst, Felix Rech

10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, Copenhagen, Denmark, ACM, January 2021

We discuss and compare two Coq mechanisations of Sierpinski's result that the generalised continuum hypothesis (GCH) implies the axiom of choice (AC). The first version shows the result, originally stated in first-order ZF set-theory, for a higher-order set theory convenient to work with in Coq. The second version presents a corresponding theorem for Coq's type theory itself, concerning type-theoretic formulations of GCH and AC. Both versions rely on the classical law of excluded middle and extensionality assumptions but we localise the use of axioms where possible.

Link to Coq formalisation

Download PDF        Show BibTeX               

@INPROCEEDINGS{KirstRech:2021:The-Generalised,
  title = {The Generalised Continuum Hypothesis Implies the Axiom of Choice in Coq},
  author = {Dominik Kirst and Felix Rech},
  year = {2021},
  month = {Jan},
  publisher = {ACM},
  booktitle = {10th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2021, Copenhagen, Denmark},
}

Login to edit