Mathematical Logic

Motivation

Ramsey's theorem says that every red/blue colouring of the pairs of an infinite set has an infinite monochromatic subset. For well-ordered sets one can ask for more: the monochromatic set should have the same order type as the whole set. Erdős and Rado introduced the partition relation $\alpha \to (\beta, c)^2$ to measure exactly this, and asked which countable ordinals $\alpha$ satisfy $\alpha \to (\alpha, 3)^2$ — every colouring either has a red copy of the whole order or a blue triangle. Such ordinals are called partition ordinals. Every partition ordinal $\alpha>1$ is a power of $\omega$, so the question becomes: for which countable $\beta$ is $\omega^\beta$ a partition ordinal? This is Erdős Problem 592.

The question is a basic test case for ordinal Ramsey theory: it is the smallest nontrivial "unbalanced" relation (a whole order type against a finite clique), and progress on it has repeatedly required new combinatorial methods.

Timeline (as recorded on erdosproblems.com/592):

• 1957 — Specker. $\omega^2 \to (\omega^2,3)^2$, and $\omega^n \not\to (\omega^n,3)^2$ for every finite $n \ge 3$.
• 1972 — Chang. $\omega^\omega \to (\omega^\omega,3)^2$ (the subject of Erdős Problem 590). Milner extended this to $\omega^\omega \to (\omega^\omega,m)^2$ for all finite $m$; Larson (1973) gave a short proof.
• 1974 — Galvin and Larson. If $\beta \ge 3$ and $\omega^\beta$ is a partition ordinal then $\beta$ is additively indecomposable, so $\beta=\omega^\gamma$. They conjectured that every such $\beta\ge3$ works.
• 2010 — Schipperus. Writing $\beta=\omega^\gamma$: the relation holds when $\gamma$ is a sum of one or two indecomposable ordinals, and fails when $\gamma$ is a sum of four or more. This refutes the Galvin–Larson conjecture in general.

The case where $\gamma$ is a sum of exactly three indecomposable ordinals appears to be the remaining open case.

Setting

An ordinal $\alpha$ is identified with a well-ordered set $X_\alpha$ of order type $\alpha$. A red/blue colouring of the complete graph $K_\alpha$ on $X_\alpha$ assigns to every pair of distinct vertices exactly one of two colours; equivalently, it is a pair of complementary simple graphs (red, blue) on $X_\alpha$.

For ordinals $\alpha,\beta$ and a cardinal $c$, the partition relation $\alpha \to (\beta,c)^2$ holds when every red/blue colouring of $K_\alpha$ has

• a set $S \subseteq X_\alpha$, all of whose pairs are red, whose order type (with the order inherited from $X_\alpha$) is exactly $\beta$, or
• a set $T \subseteq X_\alpha$, all of whose pairs are blue, with $|T| = c$.

The Lean predicate is Erdos592.OrdinalCardinalRamsey α β c, following the encoding used by the Formal Conjectures project. A partition ordinal is an $\alpha$ with $\alpha \to (\alpha,3)^2$.

An ordinal is additively indecomposable if it is nonzero and $a+b<\beta$ for all $a,b<\beta$; the additively indecomposable ordinals are exactly the powers $\omega^\delta$. An ordinal $\gamma$ is the sum of $k$ indecomposable ordinals when

$$\gamma = \omega^{\delta_1}+\cdots+\omega^{\delta_k}, \qquad \delta_1 \ge \cdots \ge \delta_k,$$

i.e. its Cantor normal form has $k$ terms counted with multiplicity. The Lean predicate is Erdos592.IsSumOfIndecomposables k γ.

Formalization targets

Goal: the three-term case

$$\gamma \text{ countable},\ \gamma=\omega^{\delta_1}+\omega^{\delta_2}+\omega^{\delta_3}\ (\delta_1\ge\delta_2\ge\delta_3) \;\Longrightarrow\; \omega^{\omega^\gamma} \to \left(\omega^{\omega^\gamma}, 3\right)^2 .$$

This is the positive answer in the open case, as predicted by the Galvin–Larson conjecture. Because the truth is unknown, a formal disproof (exhibiting a countable $\gamma$ with three Cantor-normal-form terms for which the relation fails) is an equally valid resolution of the goal. Together with the milestones below, a proof of the goal gives a complete answer to Problem 592: for countable $\beta$, $\omega^\beta$ is a partition ordinal iff $\beta\le2$ or $\beta=\omega^\gamma$ with $\gamma$ a sum of at most three indecomposables.

Milestones (known results)

1. Specker: $\omega^2 \to (\omega^2,3)^2$.
2. Specker: $\omega^n \not\to (\omega^n,3)^2$ for $3 \le n < \omega$.
3. Chang: $\omega^\omega \to (\omega^\omega,3)^2$.
4. Galvin–Larson: $\beta \ge 3$ countable and $\omega^\beta \to (\omega^\beta,3)^2$ imply that $\beta$ is additively indecomposable.
5. Schipperus: $\gamma$ countable and a sum of one or two indecomposables imply $\omega^{\omega^\gamma} \to (\omega^{\omega^\gamma},3)^2$.
6. Schipperus: $\gamma$ countable and a sum of $k \ge 4$ indecomposables imply $\omega^{\omega^\gamma} \not\to (\omega^{\omega^\gamma},3)^2$.

Significance

The result itself. A resolution of the three-term case would, together with the results above, finish the classification of countable partition ordinals of the form $\omega^\beta$ asked for in Problem 592. Either answer is informative: a positive answer shows the threshold between the positive and negative cases lies between three and four terms, and a negative answer shows it lies between two and three.

Formalizing it. The drafter is not aware of any of the milestone results in Mathlib. The Formal Conjectures entry for Problem 590 links an external Lean formalization of Chang's theorem; the other results (Specker's positive and negative theorems, Galvin–Larson, Schipperus) have, to the best of the drafter's knowledge, no public machine-checked proofs. Formalizing them is a substantial project on its own, independent of the open case, and the goal itself is an open research problem.

Difficulty

The property is not monotone in $\beta$: it holds for $\beta=2$, fails for every finite $\beta\ge3$, holds again for $\beta=\omega$, and, by Schipperus, both holds and fails for various larger $\beta=\omega^\gamma$ depending on the number of terms in the Cantor normal form of $\gamma$. So no induction on $\beta$ can settle the question, and a naive transfer of the argument for a smaller exponent to a larger one can fail. The known positive and negative results use different arguments, and the three-term case lies exactly on the boundary between the ranges they cover.

Formalization scope

• Ordinals and cardinals are Mathlib's Ordinal.{u} and Cardinal.{u} in an arbitrary universe u; "countable" is γ.card ≤ ℵ₀.
• The graph lives on α.ToType, the canonical well-ordered type of order type α; a colouring is a pair of complementary SimpleGraphs (IsCompl red blue). A red $K_\beta$ is a red clique s with typeLT s = β; a blue $K_3$ is a blue clique of cardinality exactly 3.
• IsSumOfIndecomposables k γ requires a non-increasing list of exponents of length exactly k; without the ordering requirement, "sum of $k$" would not be well defined, since for instance $\omega+\omega^2=\omega^2$.
• ω ^ ω ^ γ means $\omega^{(\omega^\gamma)}$.
• The Galvin–Larson milestone states additive indecomposability directly as $\forall a,b<\beta,\ a+b<\beta$ (for $\beta \ge 3$ this is equivalent to $\beta=\omega^\gamma$).

The goal is not trivially satisfiable: the hypotheses hold, for example, for $\gamma=3$ and $\gamma=\omega^2+\omega+1$, and the conclusion is a genuine partition relation on an infinite ordinal.

Useful reusable infrastructure includes Cantor-normal-form combinatorics for countable ordinals, order-type calculations for subsets of $\omega^\beta$, and a library of the classical colourings (Specker-type constructions). Contributions formalizing any milestone are welcome.

Selected references

• T. F. Bloom, Erdős Problem #592, erdosproblems.com. https://www.erdosproblems.com/592 (this page lists the original references [Sp57], [Ch72], [GaLa74], [Sc10] cited below).
• E. Specker, Teilmengen von Mengen mit Relationen, Comment. Math. Helv., 1957.
• C. C. Chang, A partition theorem for the complete graph on $\omega^\omega$, J. Combinatorial Theory Ser. A, 1972.
• J. A. Larson, A short proof of a partition theorem for the ordinal $\omega^\omega$, Ann. Math. Logic, 1973/74.
• F. Galvin and J. Larson, Pinning countable ordinals, Fund. Math., 1974/75.
• R. Schipperus, Countable partition ordinals, Ann. Pure Appl. Logic, 2010.
• Formal Conjectures (Google DeepMind), Erdős Problems 590–592. https://github.com/google-deepmind/formal-conjectures