GCH implies AC, a Metamath Formalization
Mario Carneiro
TL;DR
This paper formalizes Specker's proof that the Generalized Continuum Hypothesis implies the Axiom of Choice within the Metamath system, addressing complexities in canonical constructions and Cantor's normal form.
Contribution
It provides a detailed Metamath formalization of Specker's argument, clarifying previously glossed-over details in the original proof.
Findings
Successful formalization of Specker's proof in Metamath
Clarification of complexities in canonical constructions
Enhanced understanding of GCH implying AC
Abstract
We present the formalization of Specker's "local" version of the claim that the Generalized Continuum Hypothesis implies the Axiom of Choice, with particular attention to some extra complications which were glossed over in the original informal proof, specifically for "canonical" constructions and Cantor's normal form.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Logic, Reasoning, and Knowledge · Logic, programming, and type systems