Partition calculus

DefinitionOrdinal–cardinal Ramsey property#✓fully proved

For ordinals \(\alpha\), \(\beta\) and a cardinal \(c\), the partition property \(\alpha \to (\beta, c)^2\) holds if for every coloring of the edges of the complete graph on the ordinals less than \(\alpha\) in red and blue, either some set of vertices whose order type is \(\beta\) has all its edges red, or some set of vertices of cardinality exactly \(c\) has all its edges blue.

def OrdinalCardinalRamsey (α β : Ordinal.{u}) (c : Cardinal.{u}) : Prop :=
  -- For any 2-coloring of `α`,
  ∀ red blue : SimpleGraph α.ToType, IsCompl red blue →
    -- either there is a red `K_β`
    (∃ s, red.IsClique s ∧ typeLT s = β) ∨
   -- or there is a blue `K_c`.
    ∃ s, blue.IsClique s ∧ #s = c

Used by 1

Used byErdős Problem 591

DefinitionHomogeneous set#✓fully proved

Let \(c\) assign a colour in \(\gamma\) to each finite subset of a type \(I\), and let \(n \in \mathbb{N}\). A set \(H \subseteq I\) is homogeneous for \(c\) with colour \(k \in \gamma\) if \(c(s) = k\) for every \(n\)-element subset \(s\) of \(H\).

Only the values of \(c\) on \(n\)-element sets matter, so \(c\) plays the role of a colouring \([I]^n \to \gamma\) of the \(n\)-element subsets of \(I\).

def IsHomogeneousFor {I : Type*} {γ : Type*} (n : ℕ) (c : Finset I → γ) (H : Set I) (k : γ) : Prop :=
  ∀ s : Finset I, s.card = n → (s : Set I) ⊆ H → c s = k

Used by 1

Used byWeakly compact cardinal

DefinitionPartition relation for pairs with two colours#✓fully proved

For cardinals \(\kappa\) and \(\mu\), the relation \(\kappa \to (\mu)^2_2\) holds if for every set \(X\) of cardinality \(\kappa\) and every symmetric colouring \(c\) of the ordered pairs of elements of \(X\) with two colours, there are a subset \(H \subseteq X\) of cardinality \(\mu\) and a colour \(b\) such that \(c(x, y) = b\) for all distinct \(x, y \in H\).

def ArrowsPairs (κ μ : Cardinal.{0}) : Prop :=
  ∀ (α : Type), #α = κ → ∀ c : α → α → Bool, (∀ x y, c x y = c y x) →
    ∃ H : Set α, #H = μ ∧ ∃ b : Bool, ∀ x ∈ H, ∀ y ∈ H, x ≠ y → c x y = b

Used by 1

Used byErdős Problem 1219: a partition relation for sums of powers of two

DefinitionErdős Problem 1219: a partition relation for sums of powers of two#✓fully proved

The statement that for every strictly increasing sequence \(n_0 < n_1 < \cdots\) of natural numbers such that the cardinals \(2^{\aleph_{n_k}}\) are strictly increasing in \(k\) and \(2^{\aleph_{n_0}} > \aleph_\omega\), the partition relation \(\sum_k 2^{\aleph_{n_k}} \to (\aleph_\omega)^2_2\) holds: for every set \(X\) of cardinality \(\sum_k 2^{\aleph_{n_k}}\) and every symmetric colouring of the pairs of elements of \(X\) with two colours, some subset of \(X\) of cardinality \(\aleph_\omega\) has all pairs of distinct elements of the same colour.

def alephOmegaPartitionOfCardinalSum : Prop :=
  ∀ n : ℕ → ℕ, StrictMono n → StrictMono (fun k => (2 : Cardinal.{0}) ^ ℵ_ (n k)) →
    ℵ_ Ordinal.omega0 < (2 : Cardinal.{0}) ^ ℵ_ (n 0) →
      ArrowsPairs (Cardinal.sum fun k : ℕ => (2 : Cardinal.{0}) ^ ℵ_ (n k)) (ℵ_ Ordinal.omega0)

Uses 1 · Used by 1

Statement usesPartition relation for pairs with two colours

Used byShelah's theorem (Erdős Problem 1219)

TheoremShelah's theorem (Erdős Problem 1219)#●ready to prove

For every strictly increasing sequence \(n_0 < n_1 < \cdots\) of natural numbers such that the cardinals \(2^{\aleph_{n_k}}\) are strictly increasing in \(k\) and \(2^{\aleph_{n_0}} > \aleph_\omega\), the partition relation \(\sum_k 2^{\aleph_{n_k}} \to (\aleph_\omega)^2_2\) holds: for every set \(X\) of cardinality \(\sum_k 2^{\aleph_{n_k}}\) and every symmetric colouring of the pairs of elements of \(X\) with two colours, some subset of \(X\) of cardinality \(\aleph_\omega\) has all pairs of distinct elements of the same colour.

public theorem_wanted alephOmegaPartitionOfCardinalSum_holds : alephOmegaPartitionOfCardinalSum

Sources

• T. F. Bloom, Erdős Problems, Problem #1219, https://www.erdosproblems.com/1219 (status PROVED); resolution: S. Shelah, Notes on partition calculus, in Infinite and Finite Sets (Colloq. Keszthely, 1973), Colloq. Math. Soc. János Bolyai 10, North-Holland (1975), 1257-1276, erdosproblems.com/1219: proved by Shelah (a problem of Erdős, Hajnal and Rado; P. Komjáth, The Erdős-Hajnal problem list, Bull. Symb. Log. (2025), p. 2).

Uses 1

Statement usesErdős Problem 1219: a partition relation for sums of powers of two

DefinitionErdős Problem 591#✓fully proved

The statement that, for \(\alpha = \omega^{\omega^2}\), every red/blue colouring of the edges of the complete graph on the ordinals less than \(\alpha\) (that is, every pair of complementary simple graphs, red and blue, on this set) has a red clique whose order type is \(\alpha\) or a blue clique with exactly \(3\) elements. In partition notation, \(\alpha \to (\alpha, 3)^2\).

def conjecture : Prop :=
  OrdinalCardinalRamsey (ω ^ ω ^ 2 : Ordinal.{u}) (ω ^ ω ^ 2 : Ordinal.{u}) (3 : Cardinal.{u})

Uses 1 · Used by 1

Statement usesOrdinal–cardinal Ramsey property

Used byErdős Problem 591 is true

TheoremErdős Problem 591 is true#●ready to prove

Let \(\alpha = \omega^{\omega^2}\). For every red/blue colouring of the edges of the complete graph on the ordinals less than \(\alpha\), that is, every pair of complementary simple graphs (red and blue) on this set, there is a red clique whose order type is \(\alpha\) or a blue clique with exactly \(3\) elements. In partition notation, \(\alpha \to (\alpha, 3)^2\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Schipperus [Sc10] and Darby, independently, per erdosproblems.com/591, https://www.erdosproblems.com/591.

Uses 1

Statement usesErdős Problem 591

DefinitionOrdinal partition relation#✓fully proved

For an ordinal \(\alpha\) and a natural number \(n\), the partition relation \(\alpha \to (\alpha, n)^2\) holds when every colouring of the pairs \(x < y\) of ordinals below \(\alpha\) in red and blue has a red set of order type \(\alpha\) or a blue set of size \(n\): either there is a strictly increasing map \(f\) from the ordinals below \(\alpha\) to the ordinals below \(\alpha\) such that the pair \(\{f(x), f(y)\}\) is red for all \(x < y < \alpha\), or there is a set of \(n\) ordinals below \(\alpha\) all of whose pairs are blue.

def PartitionRel (α : Ordinal.{0}) (n : ℕ) : Prop :=
  ∀ c : Ordinal.{0} → Ordinal.{0} → Bool,
    (∃ f : Ordinal.{0} → Ordinal.{0}, StrictMonoOn f (Set.Iio α) ∧ (∀ x < α, f x < α) ∧
      ∀ x < α, ∀ y < α, x < y → c (f x) (f y) = true) ∨
    (∃ s : Finset Ordinal.{0}, s.card = n ∧ (∀ x ∈ s, x < α) ∧
      ∀ x ∈ s, ∀ y ∈ s, x < y → c x y = false)

Used by 1

Used byErdős Problem 118 for ordinals

DefinitionErdős Problem 118 for ordinals#✓fully proved

The statement that for every ordinal \(\alpha\) satisfying the partition relation \(\alpha \to (\alpha, 3)^2\) and every natural number \(n \ge 3\), the ordinal \(\alpha\) also satisfies \(\alpha \to (\alpha, n)^2\).

def partitionOrdinalTriangleImpliesClique : Prop :=
  ∀ α : Ordinal.{0}, PartitionRel α 3 → ∀ n : ℕ, 3 ≤ n → PartitionRel α n

Uses 1 · Used by 1

Statement usesOrdinal partition relation

Used byErdős Problem 118 fails for ordinals

TheoremErdős Problem 118 fails for ordinals#●ready to prove

There exist an ordinal \(\alpha\) satisfying the partition relation \(\alpha \to (\alpha, 3)^2\) and a natural number \(n \ge 3\) such that \(\alpha\) does not satisfy \(\alpha \to (\alpha, n)^2\).

Schipperus and Darby independently answered the question in the negative. A concrete counterexample is \(\alpha = \omega^{\omega^2}\) with \(n = 5\): Schipperus proved \(\omega^{\omega^\beta} \to (\omega^{\omega^\beta}, 3)^2\) when \(\beta\) is a sum of two additively indecomposable ordinals (here \(\beta = 1 + 1\)), and Larson proved \(\omega^{\omega^\beta} \not\to (\omega^{\omega^\beta}, 5)^2\) for every \(\beta\) that is not additively indecomposable.

public theorem_wanted partitionOrdinalTriangleImpliesClique_refuted :
    ¬ partitionOrdinalTriangleImpliesClique

Sources

• T. F. Bloom, Erdős Problems, Problem #118, https://www.erdosproblems.com/118 (status DISPROVED); resolution: R. Schipperus, Countable partition ordinals, Ann. Pure Appl. Logic 161 (2010), 1195-1215; C. Darby, Negative partition relations for ordinals ω^{ω^α}, J. Combin. Theory Ser. B 76 (1999), 205-222; J. A. Larson, An ordinal partition avoiding pentagrams, J. Symbolic Logic 65 (2000), 969-978, erdosproblems.com/118: answered no independently by Schipperus and Darby; for α = ω^{ω²}: ω^{ω²} → (ω^{ω²}, 3)² (Schipperus: ω^{ω^β} → (ω^{ω^β}, 3)² when β is a sum of two additively indecomposable ordinals) and ω^{ω²} ↛ (ω^{ω²}, 5)² (Larson, main theorem: ω^{ω^β} ↛ (ω^{ω^β}, 5)² for β not additively indecomposable; zbMATH 0967.03042); Hajnal-Larson, Handbook of Set Theory, Chapter 2.9.

Uses 1

Statement usesErdős Problem 118 for ordinals

7 fully proved3 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.