Mathematical Logic

Introduction

The Cook-Levin theorem states that CNF SAT is NP-complete. This mission formalizes the theorem over a multi-tape Turing machine model in Lean 4.

Main Goal

Prove CookLevin.cook_levin_theorem:

under the decider and reduction hypotheses.

Motivation

A Diophantine representation translates membership in a computably enumerable set into solvability of one polynomial equation. The source asks whether the entire auxiliary witness can always be made unique. The source is OpenAI's September 2026 manuscript.

Setting

A single-fold representation uses an integer polynomial evaluated at natural-number inputs and witnesses. An input belongs to the represented set exactly when a witness makes the polynomial zero, and any two complete witnesses at the same input must coincide.

Formalization targets

The proposition MainStatement holds, which asserts a single-fold Diophantine representation result with positive lengths. For every n ≥ 1 and every set S of n-tuples of natural numbers that is recursively enumerable (the predicate a ∈ S is REPred, i.e. semi-decidable), there exist m ≥ 1 and an integer polynomial P in the n input variables and m witness variables such that P represents S. Here evaluation takes natural-number inputs a and witnesses w, casts them to integers, and evaluates P over ℤ. Representation means that for every input a, first, a lies in S exactly when some witness w ∈ ℕ^m satisfies P(a,w)=0, and second, any two witnesses w and v with P(a,w)=0 and P(a,v)=0 are equal. So there is exactly one witness for members of S and none for nonmembers, and the uniqueness condition is imposed on every input a, with all witness coordinates included in w.

The goal is OAI.SingleFold.main.

Significance

The target strengthens mere existential representation by enforcing uniqueness across every auxiliary coordinate. It covers all recursively enumerable sets of positive-length natural tuples. The manuscript presents a mathematical argument; the attached goal currently has status Open, so the requested contribution is a Lean proof of the displayed formal target.

Difficulty

Encoding a computation with extra witnesses can introduce many choices that do not affect the represented input. Every such auxiliary choice must be controlled, rather than leaving hidden coordinates outside the uniqueness assertion.

Formalization scope

The input length and witness length are positive naturals. REPred expresses recursive enumerability. Polynomial coefficients and evaluation are integral, while variables range over naturals cast into the integers. The goal is existential and does not require one fixed universal polynomial.

The shared definitions are supplied by SingleFold. The target uses Lean 4.33.1 with the pinned Mathlib environment. Contributions should preserve the existing statement and develop reusable supporting lemmas in its definitions.

Selected references

• OpenAI, Single-fold Diophantine representations, preprint, September 2026. Manuscript.
• OpenAI, accompanying Lean statement. Pinned source.

Motivation: categoricity transfer beyond first-order logic

A class of structures is categorical in a cardinal $\lambda$ if it has exactly one model of size $\lambda$ up to isomorphism. Morley's theorem (1965) says that a complete first-order theory in a countable language categorical in one uncountable cardinal is categorical in all of them. Abstract elementary classes (AECs), introduced by Shelah in the 1970s, axiomatize classes of structures with a well-behaved notion of strong substructure (closure under isomorphism, coherence, unions of chains, a Löwenheim–Skolem number) without requiring first-order axiomatizability; they cover classes defined in infinitary logics and many classes of modules. Shelah's categoricity conjecture for AECs, in its eventual form, asks whether categoricity in one sufficiently large cardinal transfers to all sufficiently large cardinals. A sharper, prescribed-threshold form names the threshold explicitly: with $H(K)=\beth_{(2^{\mathrm{LS}(K)})^+}$ (the Hanf number for existence of arbitrarily large models), categoricity in some $\lambda\ge H(K)$ should imply categoricity in every $\mu\ge H(K)$. Deciding which form holds is a central question in non-elementary model theory.

Timeline

• 1965 — Morley proves the categoricity theorem for countable first-order theories (Trans. AMS 1965).
• 1970s — Shelah introduces abstract elementary classes (see the survey of Boney–Vasey 2017, §2).
• 1990 — Hart and Shelah show categoricity in $L_{\omega_1,\omega}$ can stop at $\aleph_k$ while holding for $\aleph_0,\dots,\aleph_{k-1}$, using finite-support group constructions (Israel J. Math. 1990).
• 1999 — Shelah proves categoricity transfer for AECs with amalgamation and records $H(K)$ as the existence bound (APAL 1999).
• 2016 — Kolesnikov and Lambie-Hanson study Hanf numbers for amalgamation of coloring classes (JSL 2016).
• 2017 — Vasey proves downward transfer from a successor cardinal $\ge H(K)$ under amalgamation and tameness (APAL 2017).
• 2021 — Grossberg distinguishes the prescribed-bound and eventual forms of the conjecture (A Course in Model Theory I, draft, Ch. 2 §4).
• 2022–2023 — Espíndola announces a proof of eventual categoricity and, for arbitrary AECs, a transfer at the prescribed bound via accessible categories (arXiv:1906.09169, arXiv:2301.13167).
• 2024 — Šaroch and Trlifaj state the prescribed-threshold formulation with both endpoints included (Bull. LMS 2024, §2.3).
• 2026 — An OpenAI preprint, A CH obstruction to a prescribed categoricity threshold (OpenAI Math Release, September 24, 2026), claims that under CH there is an AEC with $\mathrm{LS}(K)=\aleph_0$, categorical on a tail but with two nonisomorphic models at $H(K)=\beth_{\omega_2}$; this conflicts with the transfer claimed in Espíndola 2023 (Theorem 4.1). The preprint has not been peer reviewed and its theorem is not formally verified.

Setting

Work with relational structures in a finitary relational language $L$ (a set of relation symbols, each with a finite arity). An abstract elementary class is a class $K$ of $L$-structures with a relation $M\preceq_K N$ ("strong substructure") such that: $\preceq_K$ is a partial order on $K$ refining substructure; $K$ and $\preceq_K$ are closed under isomorphism; coherence holds ($M_0\subseteq M_1$, $M_0\preceq_K M_2$, $M_1\preceq_K M_2$ imply $M_0\preceq_K M_1$); unions of $\preceq_K$-chains are in $K$, are $\preceq_K$-extensions of each member, and are $\preceq_K$-below any common strong extension (Tarski–Vaught chain axioms); and there is a Löwenheim–Skolem number $\mathrm{LS}(K)\ge\aleph_0+|L|$, the least $\theta$ such that every subset $A$ of a model $M$ lies in some $N\preceq_K M$ with $|N|\le|A|+\theta$.

$K$ is categorical in $\mu$ if it has a model of size $\mu$ and any two models of size $\mu$ are isomorphic. The beth numbers are $\beth_0=\aleph_0$, $\beth_{\alpha+1}=2^{\beth_\alpha}$ and suprema at limits. CH is $2^{\aleph_0}=\aleph_1$.

Formalization targets

Goal: the CH counterexample (Theorem 1.1)

Assume CH. There is a countable finitary relational language $L$ and an AEC $K$ in $L$ such that

$K$ has two nonisomorphic models of cardinality $\beth_{\omega_2}$, and, with $\Lambda=\beth_{(2^{\aleph_1})^+}$,

Hence $\Lambda^+>H(K)$ is a categoricity cardinal from which downward transfer to $H(K)$ fails, while eventual categoricity holds for this $K$. The goal statement is published on the platform with status Open: no machine-checked proof exists yet.

Significance

The result itself. Combined with Gödel's relative consistency of CH, the theorem shows that, if ZFC is consistent, the prescribed-threshold form of Shelah's categoricity conjecture is not provable in ZFC (Corollary 6.1 of the source). The example has no amalgamation or joint embedding, which explains why transfer theorems that assume these properties are unaffected, and it is compatible with qualitative eventual categoricity. It also bears directly on a published claim of transfer at the prescribed bound for arbitrary AECs.

Formalizing it. Because the result contradicts a claimed theorem in the literature, an independent machine check is especially valuable. The formal statement verifies every AEC axiom explicitly, not just the two cardinal-arithmetic conclusions. Mathlib has cardinal and ordinal arithmetic, beth numbers and ZFC sets; the AEC framework built here would be reusable for further formal work in non-elementary model theory.

Difficulty

Most known non-transfer examples (Hart–Shelah) fail categoricity at small cardinals; here the failure must happen exactly at the Hanf-type bound $\beth_{\omega_2}$ while categoricity holds on a tail, with $\mathrm{LS}(K)=\aleph_0$. One must build two nonisomorphic models at $\beth_{\omega_2}$ and simultaneously rule out any two nonisomorphic models above $\Lambda$, without appealing to a general eventual-categoricity theorem. All AEC axioms — in particular coherence and smoothness of unions of arbitrary directed chains — must survive the exceptional sets used to separate models, which is where naive constructions break.

Formalization scope

• Structures are RelModel L with carrier a ZFSet (so cardinalities are cardinals of genuine sets in universe u) and relations indexed by arity; $L:\mathbb N\to$ Type with $\Sigma_n L_n$ countable.
• ClassData packages a predicate of objects and a strong-substructure relation; IsAEC lists the axioms above, including invariance under isomorphisms compatible with inclusion, coherence, and the union axioms for chains indexed by any nonzero ordinal.
• HasLSNumber ℵ₀ asserts both that $\aleph_0$ is a Löwenheim–Skolem bound and that it is the least one.
• hanf κ = beth (succ (2^κ)).ord, endpoint = beth (ω_2), tailThreshold = beth (succ (2^{ℵ₁})).ord. The equality endpoint = hanf ℵ₀ is part of the goal (it follows from CH).
• Categorical μ includes existence of a model of size $\mu$; TwoModels asks for two nonisomorphic models of the given size.
• CH is a hypothesis of the theorem, in the same universe; the consistency corollary is not part of the goal.

Selected references

• M. Morley, Categoricity in power, Trans. Amer. Math. Soc. (1965). https://doi.org/10.1090/S0002-9947-1965-0175782-0
• K. Gödel, The consistency of the axiom of choice and of the generalized continuum-hypothesis, Proc. Nat. Acad. Sci. USA (1938). https://doi.org/10.1073/pnas.24.12.556
• B. Hart and S. Shelah, Categoricity over P for first order T or categoricity for φ∈L_{ω1ω} can stop at ℵ_k while holding for ℵ_0,…,ℵ_{k−1}, Israel J. Math. (1990). https://doi.org/10.1007/BF02807869
• S. Shelah, Categoricity for abstract classes with amalgamation, Ann. Pure Appl. Logic (1999). https://doi.org/10.1016/S0168-0072(98)00016-5
• S. Vasey, Downward categoricity from a successor inside a good frame, Ann. Pure Appl. Logic (2017). https://doi.org/10.1016/j.apal.2016.10.003
• W. Boney and S. Vasey, A survey on tame abstract elementary classes, 2017. https://arxiv.org/abs/1512.00060
• A. Kolesnikov and C. Lambie-Hanson, The Hanf number for amalgamation of coloring classes, J. Symb. Logic (2016). https://doi.org/10.1017/jsl.2015.48
• J. Šaroch and J. Trlifaj, Deconstructible abstract elementary classes of modules and categoricity, Bull. London Math. Soc. (2024). https://doi.org/10.1112/blms.13172
• C. Espíndola, A complete classification of categoricity spectra of accessible categories with directed colimits, preprint, 2023. https://arxiv.org/abs/2301.13167
• OpenAI, A CH obstruction to a prescribed categoricity threshold, OpenAI Math Release preprint, September 24, 2026 (source of the goal; Theorem 1.1, p. 2). https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/preprints/A-CH-Obstruction-to-a-Prescribed-Categoricity-Threshold-September-24-2026/paper.pdf

Motivation

In 1998 Smale listed eighteen problems for the twenty-first century; the eighteenth asks: What are the limits of intelligence, both artificial and human? (Smale 1998). The paper of Acharjee and Gogoi (arXiv:2310.10792) proposes a mathematical model of a mind, the cognitive-consequence space, built from a Tarski consequence operator, and claims that two theorems about this model (its Theorems 3.3 and 3.4) show that "human intelligence is limitless" (Discussion, p. 22; Conclusion, p. 23).

This mission records that model and its results in Lean 4 exactly as stated, so that each claim becomes a checkable statement: proved, or refuted, by the verifier rather than by argument.

Setting

A cognitive-consequence space is a set $C$ of mental representations (thoughts) with a consequence operator $\mathrm{Cn} : \mathcal P(C) \to \mathcal P(C)$ and an implication connective $X \Rightarrow Y$ satisfying Tarski's axioms as listed in the paper (p. 5):

1. $C$ is countable;
2. $A \subseteq \mathrm{Cn}(A)$;
3. $A \subseteq B \Rightarrow \mathrm{Cn}(A) \subseteq \mathrm{Cn}(B)$;
4. $\mathrm{Cn}(\mathrm{Cn}(A)) = \mathrm{Cn}(A)$;
5. if $X \in \mathrm{Cn}(A)$ then $X \in \mathrm{Cn}(B)$ for some finite $B \subseteq A$;
6. if $Y \in \mathrm{Cn}(A \cup \{X\})$ then $(X \Rightarrow Y) \in \mathrm{Cn}(A)$;

together with the paper's standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$ (p. 5, after Definition 3.2).

A set $A$ is deductive if $\mathrm{Cn}(A) = A$. The cognitive-consequence topology is

and members of $\tau$ are consequence-wise open (CWO). The cognitive closure $\mathrm{Cl}^{\square}(A)$ is the intersection of all deductive sets containing $A$.

Separately, a cognitive similarity distance is a function $\mathrm{Cog} : C \times C \to [0,1]$ together with a relation $x \approx y$ ("$x$ and $y$ cognitively coincide") such that $\mathrm{Cog}(x,y) = 0 \iff x \approx y$, $\mathrm{Cog}$ is symmetric, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality holds. A sequence of thoughts $(x_n)$ converges to $x$ if for every $\varepsilon \in (0,1)$ we have $\mathrm{Cog}(x, x_n) < \varepsilon$ for all large $n$.

Formalization targets

Goal: "human intelligence is limitless" (Theorems 3.3 and 3.4)

For every cognitive-consequence space,

Milestones

Theorems 3.1, 3.2, 3.3, 3.5, 3.6, 3.7 and Corollary 3.5 (the topology $\tau$ and the cognitive closure), Theorems 3.8 and 3.12 (cognitive limits), Theorem 4.3 (the filter $f_d$) and Theorem 5.1 (Gödel's incompleteness black hole).

Significance

The paper presents the goal as its answer to the human-intelligence half of Smale's eighteenth problem. A machine-checked verdict on the goal settles whether that conclusion follows from the paper's own axioms. The milestones are the paper's structural results about $\tau$, cognitive closure and cognitive limits.

Status: to the best of current knowledge none of these results has a published machine-checked proof. The first conjunct of the goal (Theorem 3.3) follows from the standing assumption $\mathrm{Cn}(\varnothing) \neq \varnothing$. The second conjunct (Theorem 3.4) is not implied by the listed axioms as formalized: the consequence operator with $\mathrm{Cn}(A) = C$ for every $A$, on a one-point language, satisfies all of them and has $\tau = \{\varnothing\}$. The goal is therefore expected to be resolved by a disproof.

Difficulty

The content of the goal is the existence of a nonempty CWO set, equivalently of a deductive set different from $C$ (a consistent theory). The paper's argument for Theorem 3.4 derives $\bigcap_i A_i = \varnothing$ and calls this a contradiction; nothing in the axioms forbids it.

Formalization scope

• CogCons.CognitiveConsequenceSpace C bundles $\mathrm{Cn}$, the connective imp, axioms (i)–(vi) and $\mathrm{Cn}(\varnothing) \neq \varnothing$. The syntax $\sigma$ and interpretation $I$ of the paper are not modelled beyond imp.
• The paper also asserts $\mathrm{Cn}(C) \neq C$ (p. 5). This contradicts axiom (ii), since $C \subseteq \mathrm{Cn}(C) \subseteq C$; including it would make every statement vacuously true, so it is omitted. For the same reason the second half of Corollary 3.4 ($\mathrm{Cl}^{\square}(C) \neq C$) is not included.
• Theorem 4.4 (the family $\{A : f \in \mathrm{Cn}(A)\}$ is a filter) is not included: closure under intersection fails in a four-element model satisfying all the axioms.
• Results relying on informal notions (the practical topology of Section 2, Theorems 3.9–3.11 and 3.13, Theorems 4.1–4.2, and the "solution space" of Section 5) are not formalized.
• CogCons.CognitiveSimilarityDistance C is independent of $\mathrm{Cn}$; sequences are indexed by $\mathbb N$ starting at $0$; $\approx$ is an arbitrary relation constrained only by the listed axioms.

Selected references

• S. Acharjee, U. Gogoi, The limit of human intelligence, arXiv:2310.10792v2 [math.GM], 2023. https://arxiv.org/abs/2310.10792
• S. Smale, Mathematical problems for the next century, The Mathematical Intelligencer 20(2), 7–15, 1998. https://doi.org/10.1007/BF03025291

Motivation

How large can the power set of an infinite set be? For a regular cardinal $\kappa$ (one that is not the supremum of fewer than $\kappa$ smaller ordinals) the answer is: almost anything. Easton's theorem (1970) shows that the function $\kappa \mapsto 2^{\kappa}$ on regular cardinals can be prescribed arbitrarily in any model of ZFC, subject only to monotonicity and König's inequality $\operatorname{cf}(2^{\kappa}) > \kappa$. For a long time it was expected that singular cardinals — those that are such a supremum, like $\aleph_{\omega}$ — would behave the same way.

They do not. In 1974 Jack Silver proved that the Generalized Continuum Hypothesis cannot fail for the first time at a singular cardinal of uncountable cofinality: if $2^{\alpha} = \alpha^{+}$ for every infinite $\alpha < \kappa$ and $\operatorname{cf}\kappa > \omega$, then $2^{\kappa} = \kappa^{+}$. This was the first ZFC theorem constraining the continuum function at singular cardinals, and it opened the area now called the singular cardinal problem.

A short timeline:

• 1970 — Easton: the continuum function on regular cardinals is essentially arbitrary.
• 1974 — Silver (ICM Vancouver): GCH cannot first fail at a singular cardinal of uncountable cofinality; more generally the Singular Cardinal Hypothesis is decided at cofinality $\omega$.
• 1975 — Galvin and Hajnal: elementary inequalities for cardinal powers at singular cardinals of uncountable cofinality.
• 1976–77 — Baumgartner and Prikry, and independently Jensen, give elementary (non-forcing, non-ultrapower) proofs of Silver's theorem; the proof reproduced in Jech's Chapter 8 is of this kind.
• 1977 — Magidor: it is consistent, relative to large cardinals, that GCH holds below $\aleph_{\omega}$ while $2^{\aleph_{\omega}} > \aleph_{\omega+1}$ — so Silver's restriction to uncountable cofinality is necessary.
• 1980s onwards — Shelah's pcf theory, whose flagship result $\aleph_{\omega}^{\aleph_0} < \aleph_{\omega_4}$ (when $\aleph_\omega$ is a strong limit) grows out of exactly the stationary-set machinery assembled here.

This mission is the first in a series formalizing Thomas Jech, Set Theory (Third Millennium Edition, Springer 2003). It covers Chapter 8, "Stationary Sets" (pp. 91–98).

Setting

Fix a regular uncountable cardinal $\kappa$ and regard it as the well-ordered set of ordinals below it. A set $C \subseteq \kappa$ is closed unbounded, or a club, if it is unbounded in $\kappa$ and contains all of its limit points below $\kappa$ (an ordinal $\alpha > 0$ is a limit point of $C$ when $\sup(C \cap \alpha) = \alpha$). A set $S \subseteq \kappa$ is stationary if $S \cap C \neq \emptyset$ for every club $C$. Clubs are closed under intersections of fewer than $\kappa$ of them, so they generate a $\kappa$-complete filter, the club filter; its dual is the nonstationary ideal.

The club filter has a second closure property with no analogue for ordinary filters. The diagonal intersection of a $\kappa$-indexed family is

and a filter closed under diagonal intersections is called normal. A function $f$ defined on $S \subseteq \kappa$ is regressive if $f(\alpha) < \alpha$ for all nonzero $\alpha \in S$.

For cardinal arithmetic, $\operatorname{cf}\kappa$ denotes the cofinality of $\kappa$ (the least length of an unbounded sequence in $\kappa$), $\kappa^{+}$ the cardinal successor, and $\kappa$ is singular when $\operatorname{cf}\kappa < \kappa$. The Singular Cardinal Hypothesis (SCH) is the assertion that $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$ for every singular $\kappa$ with $2^{\operatorname{cf}\kappa} < \kappa$. A sequence of cardinals is normal if it is strictly increasing and continuous at limits.

Formalization targets

Goal — Silver's theorem (Jech 8.12)

This is the weakest statement of the chapter that still needs the full machinery: it fixes no particular $\kappa$ and no particular cofinality, and it stays correct no matter how the singular cardinal problem develops above it.

Milestones, in dependency order

1. Lemma 8.4 — the diagonal intersection of $\kappa$ clubs is a club; equivalently the club filter is normal.
2. Theorem 8.7 (Fodor) — a regressive function on a stationary set is constant on a stationary subset.
3. Theorem 8.10 (Solovay) — every stationary subset of $\kappa$ is the union of $\kappa$ pairwise disjoint stationary sets.
4. Lemma 8.14 — if $\langle \kappa_\alpha\rangle$ is normal with limit $\kappa$, $\lambda^{\operatorname{cf}\kappa} < \kappa$ for $\lambda < \kappa$, and $\{\alpha : \kappa_\alpha^{\operatorname{cf}\kappa_\alpha} = \kappa_\alpha^{+}\}$ is stationary in $\operatorname{cf}\kappa$, then $\kappa^{\operatorname{cf}\kappa} = \kappa^{+}$.
5. Theorem 8.13 (Silver) — SCH at every cardinal of cofinality $\omega$ implies SCH everywhere.

Significance

Silver's theorem is the boundary between the two halves of cardinal arithmetic. Above it sit the ZFC theorems of pcf theory; below it sit the consistency results (Magidor, Prikry, Radin forcing) that show how much freedom is left, and they are confined to cofinality $\omega$ precisely because Theorems 8.12 and 8.13 close off everything else. Its proof also packages tools used throughout set theory: the normality of the club filter, Fodor's pressing-down lemma, and the technique of bounding almost disjoint families of functions by a stationary-set argument.

Formalization status: Mathlib already has clubs and stationary sets in an arbitrary well-ordered type (IsClub, IsStationary), with the finite and $<\kappa$-indexed intersection lemmas — Jech's Lemma 8.2 and Theorem 8.3. It does not have diagonal intersections, Fodor's theorem, Solovay's splitting theorem, or any singular cardinal arithmetic beyond the definitions of regular and singular cardinals. Each milestone below is therefore a genuine addition, and the first three are reusable well outside this mission.

Difficulty

The naive route to the goal — induct on $\alpha < \kappa$ and pass to the limit — fails immediately: $2^{\kappa}$ for singular $\kappa$ is not determined by the values $2^{\alpha}$ for $\alpha < \kappa$ in any elementary way; that is exactly the content of the independence results. What the proof must do instead is bound the number of functions on $\operatorname{cf}\kappa$, and it gets that bound from a stationary set rather than from a club: uncountable cofinality is what makes the set of relevant stages stationary, and stationarity is what survives the diagonal argument. Cofinality $\omega$ breaks this at the first step, since every subset of $\omega$ that is unbounded is already a club and Fodor's theorem is empty.

The two hard pieces are Lemma 8.14 and, inside it, Lemma 8.16: given an almost disjoint family $F$ of functions with $f(\alpha) \in A_\alpha$ and $|A_\alpha| \le \aleph_\alpha$ on a stationary set of $\alpha$, one must show $|F| \le \aleph_{\omega_1}$ by assigning to each $f$ a pair (stationary set, bounded restriction) and checking the assignment is injective. That argument uses Fodor's theorem on a set of functions, and the bookkeeping does not simplify.

Formalization scope

The ambient order is Mathlib's type of ordinals below a cardinal, k.ord.ToType (written Below k in the mission's definition bundle); clubs and stationary sets are Mathlib's IsClub and IsStationary on that type, so a set is closed in the sense of being closed under suprema of directed subsets — equivalent, for a well-order with the order topology, to Jech's "contains its limit points". Families indexed by "$\alpha < \kappa$" are functions out of that same type, which is what makes the diagonal intersection typecheck without a side condition. Cardinal exponentiation, cofinality (Ordinal.cof of k.ord) and the successor cardinal (Order.succ) are Mathlib's.

One trivializing formalization is ruled out explicitly: the GCH hypothesis of the goal is stated for infinite cardinals $\alpha < \kappa$ only. Quantified over all cardinals it would be unsatisfiable — $2^{2} = 4 \neq 3 = 2^{+}$ — and Silver's theorem would become vacuous.

A complete development needs: diagonal intersections and the normality of the club filter; Fodor's theorem; the sets $E^{\kappa}_{\lambda} = \{\alpha < \kappa : \operatorname{cf}\alpha = \lambda\}$ and their stationarity; Solovay's splitting theorem via Lemmas 8.8 and 8.9; almost disjoint families of ordinal functions and the counting Lemmas 8.15 and 8.16; and Theorem 5.22(ii) on cardinal powers, which Jech's proof of Theorem 8.13 cites. Contributions of any of these as separate reductions are welcome, as are alternative proofs of the goal (for instance via a generic elementary embedding) that bypass some of the chain.

Selected references

• Thomas Jech, Set Theory, The Third Millennium Edition, revised and expanded. Springer Monographs in Mathematics, Springer, 2003 (ISBN 3-540-44085-2). Chapter 8, "Stationary Sets", pp. 91–98 — the source of every statement in this mission.
• Jack Silver, On the singular cardinals problem. Proceedings of the International Congress of Mathematicians (Vancouver, 1974), vol. 1, pp. 265–268.
• William B. Easton, Powers of regular cardinals. Annals of Mathematical Logic 1 (1970), pp. 139–178.
• Fred Galvin and András Hajnal, Inequalities for cardinal powers. Annals of Mathematics 101 (1975), pp. 491–498.
• James E. Baumgartner and Karel Prikry, Singular cardinals and the generalized continuum hypothesis. American Mathematical Monthly 84 (1977), pp. 108–113.
• Menachem Magidor, On the singular cardinals problem I. Israel Journal of Mathematics 28 (1977), pp. 1–31.

Motivation

Cantor's continuum problem asks for the value of $2^\kappa$, the cardinality of the power set of an infinite cardinal $\kappa$. For regular cardinals ZFC says almost nothing: by Easton's theorem (1970) the function $\kappa\mapsto 2^\kappa$ on regular cardinals can be essentially any non-decreasing function with $\operatorname{cf}(2^\kappa)>\kappa$. For singular cardinals the picture is different, and the singular cardinals hypothesis (SCH) is the natural statement of "GCH-like behaviour at singular cardinals". It arose from the question whether the least cardinal at which GCH fails can be singular.

Timeline.

• Scott (1961): if GCH holds on a set of measure one below a measurable cardinal $\kappa$, then $2^\kappa=\kappa^+$.
• Solovay (1974): above a strongly compact cardinal, SCH holds.
• Silver (1975): if $\kappa$ is singular of uncountable cofinality and $2^\lambda=\lambda^+$ for all infinite $\lambda<\kappa$, then $2^\kappa=\kappa^+$. Consequently the least failure of SCH has countable cofinality.
• Silver, Prikry: from a supercompact cardinal, a model of $\neg$SCH (Prikry forcing over a measurable $\kappa$ with $2^\kappa>\kappa^+$).
• Gitik (1989–1991), building on Woodin: $\mathrm{ZFC}+\neg\mathrm{SCH}$ is equiconsistent with a measurable cardinal of Mitchell order $\kappa^{++}$.
• Todorcevic, Veličković (1980s): the proper forcing axiom implies $2^{\aleph_0}=\aleph_2$.
• Viale (2006): the proper forcing axiom implies SCH.

Setting

All cardinals live in one universe. For a cardinal $\kappa$, $\kappa^+$ is its successor cardinal and $\operatorname{cf}\kappa$ its cofinality (the cofinality of the initial ordinal of $\kappa$). A cardinal is singular if it is infinite and $\operatorname{cf}\kappa<\kappa$, and a strong limit if $\kappa\neq0$ and $2^\lambda<\kappa$ for all $\lambda<\kappa$.

• GCH: $2^\kappa=\kappa^+$ for every infinite $\kappa$.
• SCH (first form, following Mitchell 1992): $2^\kappa=\kappa^+$ for every singular strong limit $\kappa$.
• SCH$_2$ (second form): for every singular $\kappa$, $2^{\operatorname{cf}\kappa}<\kappa$ implies $\kappa^{\operatorname{cf}\kappa}=\kappa^+$.

A normal measure on $\kappa$ is a nonprincipal $\kappa$-complete ultrafilter on $\kappa$ under which every regressive function is constant on a measure-one set; $\kappa$ is measurable if it is uncountable and carries one. $\kappa$ is strongly compact if it is uncountable and every proper $\kappa$-complete filter on any set extends to a $\kappa$-complete ultrafilter. The proper forcing axiom (PFA) asserts that for every proper poset $P$ and every $\aleph_1$ dense subsets of $P$ there is a filter meeting all of them.

Formalization targets

Goal: Silver's reduction

SCH itself is independent of ZFC, so it cannot be a goal; the goal is the ZFC theorem that SCH can only first fail at countable cofinality.

Milestones (in order)

1. GCH $\Rightarrow$ SCH.
2. $\kappa^{\operatorname{cf}\kappa}=2^\kappa$ for every singular strong limit $\kappa$.
3. SCH$_2$ $\Rightarrow$ SCH.
4. Silver's theorem: $\kappa$ singular, $\operatorname{cf}\kappa>\aleph_0$, GCH below $\kappa$ $\Rightarrow$ $2^\kappa=\kappa^+$ (already published and proved on the platform as JechSetTheory.silver).
5. The second-form reduction: SCH$_2$ at all $\lambda$ of countable cofinality implies SCH$_2$ everywhere (published, open, as JechSetTheory.sch_of_sch_cof_aleph0).
6. The least counterexample to SCH has cofinality $\aleph_0$.
7. Scott's theorem: $D$ a normal measure on $\kappa$ and $\{\alpha<\kappa: 2^{|\alpha|}=|\alpha|^+\}\in D$ imply $2^\kappa=\kappa^+$.
8. Solovay's theorem: if $\kappa$ is strongly compact, then $2^\mu=\mu^+$ for every singular strong limit $\mu>\kappa$.
9. PFA $\Rightarrow 2^{\aleph_0}=\aleph_2$.
10. PFA $\Rightarrow$ SCH.

Significance

The goal locates the first possible failure of SCH: any model of $\neg$SCH must have a counterexample of countable cofinality, which is why Prikry-type forcing (which adds an $\omega$-sequence) is the standard tool for producing failures, and why $\aleph_\omega$ is the canonical test case. Milestones 1, 7, 8 and 10 show that very different hypotheses (GCH, large cardinals, forcing axioms) all imply SCH, while milestone 9 shows PFA does so without GCH.

These results are classical and have complete published proofs (Jech, Set Theory, Chapters 8, 20, 24, 31). Silver's theorem is already machine-checked on this platform; the rest, including the stationary-set form of Silver's theorem needed for the goal, are not yet formalized here.

Difficulty

The naive attempt at the goal, "apply Silver's theorem at the least counterexample", fails: Silver's theorem as stated needs GCH at all infinite cardinals below $\kappa$, but SCH below $\kappa$ says nothing about regular cardinals or non-strong-limits. The proof needs the stronger, stationary-set version of Silver's theorem (Galvin–Hajnal style), applied to the stationary set of singular strong limits of countable cofinality below $\kappa$. Scott's and Solovay's theorems need ultrapower arguments, and PFA $\Rightarrow$ SCH needs reflection and covering-type combinatorics; none of these exist in Mathlib.

Formalization scope

• Cardinals are Mathlib Cardinal.{u}; singularity is Cardinal.IsSingular, strong limit is Cardinal.IsStrongLimit, cofinality is κ.ord.cof, successor is Order.succ κ. The second form reuses the published predicate JechSetTheory.SCHAt.
• A measure on $\kappa$ is an ultrafilter on Ordinal.{u} containing the ordinals below $\kappa$; completeness quantifies over index types of universe u. "Proper filter" in the definition of strong compactness is Filter.NeBot; without it no cardinal would be strongly compact and Solovay's theorem would be vacuous.
• Properness of a poset is encoded by the Gray–Shelah game characterization (names for ordinals in maximal-antichain form, forcing unfolded into predensity), because Mathlib has no forcing relation; this encoding deserves particular scrutiny. Posets are nonempty preorders with $q\le p$ meaning $q$ is stronger.
• Not formalized: the consistency and equiconsistency results (Gitik, Prikry forcing, Silver's supercompact construction, inner-model lower bounds) and the strictness of "SCH$_2$ is stronger than SCH"; these are statements about models of ZFC rather than theorems of ZFC.
• Reusable infrastructure welcome: clubs and stationary sets on cardinals (partly available in Def_JechStationary), ultrapowers by normal measures, Fodor's lemma, Galvin–Hajnal bounds.

Selected references

• W. J. Mitchell, On the singular cardinal hypothesis, Trans. Amer. Math. Soc. 329(2), 507–530, 1992.
• J. Silver, On the singular cardinals problem, Proc. ICM Vancouver 1974, 265–268, 1975.
• T. Jech, Set Theory, 3rd millennium ed., Springer, 2003.
• M. Gitik, The strength of the failure of the singular cardinal hypothesis, Ann. Pure Appl. Logic 51, 215–240, 1991.
• M. Viale, The proper forcing axiom and the singular cardinal hypothesis, J. Symbolic Logic 71(2), 473–479, 2006.
• S. Shelah, Proper and Improper Forcing, Springer, 1998.
• Wikipedia, Singular cardinals hypothesis, revision 1349753131. https://en.wikipedia.org/w/index.php?title=Singular_cardinals_hypothesis&oldid=1349753131