1. FormalConjectures
  2. ErdosProblems
  3. «1167»
/- Copyright 2026 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 1167

Reference: erdosproblems.com/1167

The original Erdős–Hajnal problem list gives the additional conditions $\gamma \geq 2$, $r < \omega$, and $\kappa_\alpha > r$. Without $\gamma \geq 2$, the statement is false: taking $\gamma = 1$ and $\kappa_0 = \aleph_1$ with $\lambda = \aleph_0$ gives a counterexample, since the partition relation with one color degenerates to a cardinality comparison (see erdos_1167.unrestricted_is_false). Without $\kappa_\alpha > r$ it is also false: with $r = 2$, $\lambda = \aleph_0$ and targets $(2, \aleph_1)$, the premise $2^{\aleph_0} \to (3, \aleph_1)^3$ holds, but a constant colouring of the pairs of $\aleph_0$ has neither a red pair nor a blue set of size $\aleph_1$.

open Cardinal Ordinal Combinatoricsnamespace Erdos1167universe u

Erdős Problem 1167. Let $r \geq 2$ be finite, $\gamma \geq 2$, and $\lambda$ be an infinite cardinal. Let $\kappa_\alpha > r$ be cardinals for all $\alpha < \gamma$. Is it true that $$2^\lambda \to (\kappa_\alpha + 1){\alpha < \gamma}^{r+1}$$ implies $$\lambda \to (\kappa\alpha){\alpha < \gamma}^r?$$ Here $+$ means cardinal addition, so that $\kappa\alpha + 1 = \kappa_\alpha$ if $\kappa_\alpha$ is infinite.

A problem of Erdős, Hajnal, and Rado.

@[category research open, AMS 5] theorem erdos_1167 : answer(sorry) ↔ ∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), (∀ α, (r : Cardinal.{u}) < κ α) → cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => κ α + 1) → cardinalPartitionRel lam r γ κ := ⊢ True ↔ ∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}), 2 ≤ γ → ∀ (κ : γ.ToType → Cardinal.{u}), (∀ (α : γ.ToType), ↑r < κ α) → (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κ All goals completed! 🐙namespace erdos_1167.variants

Finite-target case. When all $\kappa_\alpha$ are finite, $\kappa_\alpha + 1$ is the ordinary natural-number successor. Special case of erdos_1167.

@[category research open, AMS 5] theorem finite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (n : γ.ToType → ℕ) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ (fun α => (n α : Cardinal.{u}) + 1) → cardinalPartitionRel lam r γ (fun α => (n α : Cardinal.{u})) := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γn:γ.ToType → ℕ⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ ↑(n α) + 1) → cardinalPartitionRel lam r γ fun α ↦ ↑(n α) All goals completed! 🐙

Binary-color case. The $\gamma = 2$ specialization (two color classes).

@[category research open, AMS 5] theorem binary_colors (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (κ : (2 : Ordinal.{u}).ToType → Cardinal.{u}) (hκ : ∀ α, (r : Cardinal.{u}) < κ α) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) 2 (fun α => κ α + 1) → cardinalPartitionRel lam r 2 κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamκ:ToType 2 → Cardinal.{u}hκ:∀ (α : ToType 2), ↑r < κ α⊢ (cardinalPartitionRel (2 ^ lam) (r + 1) 2 fun α ↦ κ α + 1) → cardinalPartitionRel lam r 2 κ All goals completed! 🐙

Infinite-target case. When all $\kappa_\alpha \geq \aleph_0$ are infinite and bounded by $\lambda$, $\kappa_\alpha + 1 = \kappa_\alpha$, so the hypothesis simplifies to a "pure" stepping-down lemma: $$2^\lambda \to (\kappa_\alpha){\alpha<\gamma}^{r+1} \implies \lambda \to (\kappa\alpha){\alpha<\gamma}^r.$$ The condition $\kappa\alpha \leq \lambda$ is needed to avoid a size obstruction: without it, the conclusion would require a subset of $\lambda$ of size $\kappa_\alpha > \lambda$, which is impossible (see infinite_targets_needs_bound).

@[category research open, AMS 5] theorem infinite_targets (r : ℕ) (hr : 2 ≤ r) (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ i, ℵ₀ ≤ κ i) (hκ_le : ∀ i, κ i ≤ lam) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ := r:ℕhr:2 ≤ rlam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}hκ:∀ (i : γ.ToType), ℵ₀ ≤ κ ihκ_le:∀ (i : γ.ToType), κ i ≤ lam⊢ cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κ All goals completed! 🐙

$r = 2$ case. The stepping-down from 3-uniform to 2-uniform partition relations: $2^\lambda \to (\kappa_\alpha + 1){\alpha<\gamma}^3$ implies $\lambda \to (\kappa\alpha)_{\alpha<\gamma}^2$. Generalises the classical Erdős–Rado stepping-up/down theorem for pairs.

@[category research open, AMS 5] theorem r_eq_two (lam : Cardinal.{u}) (hlam : ℵ₀ ≤ lam) (γ : Ordinal.{u}) (hγ : 2 ≤ γ) (κ : γ.ToType → Cardinal.{u}) (hκ : ∀ α, (2 : Cardinal.{u}) < κ α) : cardinalPartitionRel ((2 : Cardinal.{u}) ^ lam) 3 γ (fun α => κ α + 1) → cardinalPartitionRel lam 2 γ κ := lam:Cardinal.{u}hlam:ℵ₀ ≤ lamγ:Ordinal.{u}hγ:2 ≤ γκ:γ.ToType → Cardinal.{u}hκ:∀ (α : γ.ToType), 2 < κ α⊢ (cardinalPartitionRel (2 ^ lam) 3 γ fun α ↦ κ α + 1) → cardinalPartitionRel lam 2 γ κ All goals completed! 🐙end erdos_1167.variants

A canonical element of the type (1 : Ordinal).ToType.

noncomputable def i0 : (1 : Ordinal.{u}).ToType := default

The partition relation $\mu \to (\nu)^r_1$ with a single color is equivalent to $\nu \le \mu$.

μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #A⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0⊢ ∃ i H, #↑H = ν i ∧ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0⊢ ∀ (s : Finset A) (hs : s.card = r), ↑s ⊆ H → col ⟨s, hs⟩ = i0 μ:Cardinal.{u}r:ℕν:ToType 1 → Cardinal.{u}h:μ ≥ ν i0A:Type uhA:#A = μcol:{ s // s.card = r } → ToType 1hle:ν i0 ≤ #AH:Set AhH:#↑H = ν i0s:Finset Ahs:s.card = rhsH:↑s ⊆ H⊢ col ⟨s, hs⟩ = i0 All goals completed! 🐙

The unrestricted version of Erdős Problem 1167 (without the condition $\gamma \geq 2$ from the original Erdős–Hajnal list) is false. Taking $\gamma = 1$, $\kappa_0 = \aleph_1$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (\aleph_1 + 1)^3_1$ holds since $2^{\aleph_0} \geq \aleph_1$, but the conclusion $\aleph_0 \to (\aleph_1)^2_1$ fails since $\aleph_0 < \aleph_1$.

h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α ↦ ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ ℵ_ 1 + 1h3:ℵ₀ ≥ ℵ_ 1⊢ False h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (cardinalPartitionRel (2 ^ lam) (r + 1) γ fun α ↦ κ α + 1) → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun α ↦ ℵ_ 1 + 1) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ ℵ_ 1h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ ℵ_ 1 + 1h3:ℵ₀ ≥ ℵ_ 1h4:ℵ₀ < ℵ_ 1⊢ False All goals completed! 🐙

The infinite_targets variant without the bound $\kappa_\alpha \leq \lambda$ is false. Taking $\gamma = 1$, $\kappa_0 = 2^{\aleph_0}$, $\lambda = \aleph_0$: the premise $2^{\aleph_0} \to (2^{\aleph_0})^3_1$ holds since $2^{\aleph_0} \leq 2^{\aleph_0}$, but the conclusion $\aleph_0 \to (2^{\aleph_0})^2_1$ fails by Cantor's theorem.

h:∀ (r : ℕ), 2 ≤ r → ∀ (lam : Cardinal.{u}), ℵ₀ ≤ lam → ∀ (γ : Ordinal.{u}) (κ : γ.ToType → Cardinal.{u}), (∀ (i : γ.ToType), ℵ₀ ≤ κ i) → cardinalPartitionRel (2 ^ lam) (r + 1) γ κ → cardinalPartitionRel lam r γ κh1:(cardinalPartitionRel (2 ^ ℵ₀) (2 + 1) 1 fun x ↦ 2 ^ ℵ₀) → cardinalPartitionRel ℵ₀ 2 1 fun x ↦ 2 ^ ℵ₀h2:cardinalPartitionRel (2 ^ ℵ₀) 3 1 fun x ↦ 2 ^ ℵ₀h3:ℵ₀ ≥ 2 ^ ℵ₀⊢ False All goals completed! 🐙end Erdos1167