Model Theory

Motivation

The continuum hypothesis (CH) asks how large the set of real numbers is. Cantor proved that $|\mathbb Z|=|\mathbb Q|<|\mathbb R|$, and in 1878 he conjectured that no set has cardinality strictly between that of the integers and that of the reals. Settling CH was the first of Hilbert's problems at the 1900 International Congress of Mathematicians. The question was answered by showing that it cannot be answered from the standard axioms: CH is independent of Zermelo–Fraenkel set theory with choice (ZFC).

Timeline (as recorded in the source):

• 1878 — Cantor formulates the (weak) continuum hypothesis; in 1882 he states CH in its modern form.
• 1900 — Hilbert lists CH as the first of his problems.
• 1906 — Kőnig proves a theorem that, combined with Hausdorff's notion of cofinality (1908), shows $2^{\aleph_0}\neq\aleph_\alpha$ whenever $\alpha$ has cofinality $\omega$.
• 1930 — Patai: if $2^\kappa$ is the $\gamma$-th successor of $\kappa$ for every infinite $\kappa$, then $\gamma$ is finite.
• 1938/1940 — Gödel proves that AC and GCH hold in the constructible universe $L$, so $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$.
• 1947 — Sierpiński proves that ZF + GCH implies AC.
• 1963 — Cohen invents forcing and proves $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$.
• 1986 — Freiling shows that $\neg$CH is equivalent to his axiom of symmetry.

Setting

A cardinal measures the size of a set; $|A|\le|B|$ means there is an injection $A\to B$, and $|A|=|B|$ a bijection. $\aleph_0=|\mathbb N|$, $2^\kappa=|\mathcal P(X)|$ for $|X|=\kappa$, so $|\mathbb R|=2^{\aleph_0}$. $\aleph_\alpha$ is the $\alpha$-th infinite cardinal, $\beth_\alpha$ is defined by $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits, and $\mathrm{cf}$ denotes cofinality.

• CH: there is no $S\subseteq\mathbb R$ with $\aleph_0<|S|<2^{\aleph_0}$ (CH).
• GCH: for every infinite cardinal $\kappa$ there is no cardinal strictly between $\kappa$ and $2^\kappa$ (GCH).

Independence is a statement about a first-order theory. The language of set theory has one binary relation symbol $\in$ (setLang). ZF (ZF) consists of extensionality, foundation, pairing, union, power set, infinity, and all instances of the separation and replacement schemas; ZFC (ZFC) adds the axiom of choice (acSentence). CH and GCH are also written as first-order sentences (chSentence, gchSentence): CH says that every subset of $\mathcal P(\omega)$ injects into $\omega$ or receives an injection from $\mathcal P(\omega)$. A theory is consistent if it has a model, and $T\models\sigma$ means $\sigma$ holds in every model of $T$; by Gödel's completeness theorem these coincide with the proof-theoretic notions.

Formalization targets

Goal: independence of CH from ZFC

$$\mathrm{Con}(\mathrm{ZFC})\ \Longrightarrow\ \mathrm{ZFC}\not\models\mathrm{CH}\ \text{ and }\ \mathrm{ZFC}\not\models\neg\mathrm{CH}.$$

Milestones

1. $|\mathbb Z|=|\mathbb Q|<|\mathbb R|$.
2. $\mathrm{CH}\iff 2^{\aleph_0}=\aleph_1$.
3. (Gödel) $\mathrm{Con}(\mathrm{ZF})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\mathrm{GCH})$.
4. $\mathrm{ZFC}+\mathrm{GCH}\models\mathrm{CH}$.
5. (Cohen) $\mathrm{Con}(\mathrm{ZFC})\Rightarrow\mathrm{Con}(\mathrm{ZFC}+\neg\mathrm{CH})$.
6. (Kőnig) $2^{\aleph_0}\neq\aleph_\alpha$ when $\mathrm{cf}(\alpha)=\omega$; and $\mathrm{cf}(2^{\aleph_0})>\aleph_0$.
7. (Sierpiński) $\mathrm{ZF}+\mathrm{GCH}\models\mathrm{AC}$.
8. $\mathrm{GCH}\iff\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+1}\iff\forall\alpha,\ \aleph_\alpha=\beth_\alpha$.
9. Under GCH: $A<B\Rightarrow 2^A<2^B$ for infinite $A$, and the three-case formula for $\aleph_\alpha^{\aleph_\beta}$.
10. (Patai) $\forall\alpha,\ 2^{\aleph_\alpha}=\aleph_{\alpha+\gamma}$ implies $\gamma<\omega$.
11. (Freiling) the axiom of symmetry is equivalent to $\neg$CH.

Significance

The independence theorem shows that the ZFC axioms do not determine the size of the continuum, and it was among the first independence results for a mathematical statement. Its two halves introduced the two main tools of modern set theory: inner models (Gödel's $L$) and forcing (Cohen). Many statements in analysis, topology and measure theory were subsequently shown to be independent by the same methods.

For formalization, the goal requires a model theory of ZF inside Lean: interpreting the first-order theory, building $L$ inside an arbitrary model of ZF, and building forcing extensions of an arbitrary model of ZFC. The independence of CH was formalized in Lean 3 by the Flypitch project (Han and van Doorn, 2019–2020); no Lean 4 / Mathlib formalization is known to this mission. The cardinal-arithmetic milestones (2, 6, 8–11) are theorems of ZFC that can be proved directly in Lean's cardinal library.

Difficulty

Neither half follows from cardinal arithmetic in Lean: Lean's foundations prove that models of ZFC exist, but (assuming they are consistent) they prove neither CH nor its negation about Lean's own Cardinal, so an argument inside Lean's cardinal arithmetic alone cannot produce the required models. Gödel's half needs relativization of formulas to a definable inner class and absoluteness of the construction of $L$; Cohen's half needs a generic extension in which a new family of $\aleph_2$ reals is added while cardinals are preserved (the countable chain condition). Both require a theory of definability inside arbitrary, possibly non-well-founded, models of a first-order theory.

Formalization scope

• Syntax and semantics are Mathlib's first-order logic (FirstOrder.Language, Theory.IsSatisfiable, Theory.ModelsBoundedFormula written ⊨ᵇ). Formulas name their variables by natural numbers; close φ is the universal closure. Equality is the built-in equality of first-order logic.
• Consistency is satisfiability and provability is semantic consequence over models with universe in Type. By the completeness theorem these agree with the syntactic notions.
• The first-order CH uses $\mathcal P(\omega)$ in place of $\mathbb R$ (they are equinumerous in ZF). The first-order GCH is the choice-free form "$|S|\le|T|\le|\mathcal P(S)|\Rightarrow|T|=|S|$ or $|T|=|\mathcal P(S)|$, for $S$ infinite".
• The consistency results carry their hypotheses $\mathrm{Con}(\mathrm{ZF})$ or $\mathrm{Con}(\mathrm{ZFC})$ explicitly, even though these are provable in Lean. A solution may not replace a model of ZF by Lean's own universe in a way that assumes CH or its negation.
• Results that need large-cardinal hypotheses or class forcing (Easton, Solovay, Foreman–Woodin, Merimovich) are not part of this mission.

Reusable infrastructure: the language of set theory with standard abbreviations (pairs, functions, $\omega$, power set), satisfaction lemmas for the abbreviations, relativization, absoluteness, the constructible hierarchy, and forcing over models of ZFC.

Selected references

• G. Cantor, Ein Beitrag zur Mannigfaltigkeitslehre, J. Reine Angew. Math. 84 (1878) 242–258. https://doi.org/10.1515/crll.1878.84.242
• K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis, PNAS 24 (1938) 556–557. https://doi.org/10.1073/pnas.24.12.556
• K. Gödel, The Consistency of the Axiom of Choice and of the Generalized Continuum-Hypothesis with the Axioms of Set Theory, Annals of Math. Studies 3, Princeton, 1940.
• P. J. Cohen, The independence of the Continuum Hypothesis I, II, PNAS 50 (1963) 1143–1148; 51 (1964) 105–110. https://doi.org/10.1073/pnas.50.6.1143, https://doi.org/10.1073/pnas.51.1.105
• C. Freiling, Axioms of symmetry: throwing darts at the real number line, J. Symbolic Logic 51 (1986) 190–200. https://doi.org/10.2307/2273955
• L. Gillman, Two classical surprises concerning the Axiom of Choice and the Continuum Hypothesis, Amer. Math. Monthly 109 (2002) 544–553. https://doi.org/10.2307/2695444
• K. Kunen, Set Theory: An Introduction to Independence Proofs, North-Holland, 1980.
• Wikipedia, Continuum hypothesis (revision 1376315189). https://en.wikipedia.org/w/index.php?title=Continuum_hypothesis&oldid=1376315189