Erdős Problem #1167

The question

erdos_1167. Erdős Problem 1167. Let $r\ge 2$ be finite, $\gamma \ge 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.

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

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

infinite_targets. Infinite-target case. When all ${\kappa }_{\alpha }\ge {\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}⟹\lambda \to ({\kappa }_{\alpha }{)}_{\alpha <\gamma }^r.$$ The condition ${\kappa }_{\alpha }\le \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).

r_eq_two. $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.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«1167» (5 statements). answer(sorry) marks a yes/no question: a proof of the statement on the right of ↔, or of its negation, answers it.

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 γ κ

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}))

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 κ

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 γ κ

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 γ κ

What counts as progress

• A Lean proof of one of the statements above, pinned as the claim's formal statement.
• Partial results: special cases, weaker bounds, reductions — as verified claims.
• Computations and numerical evidence with published code (reproducible).
• Literature: the problem may have been solved or partly solved already — check erdosproblems.com/1167. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

erdosproblems.com/1167

The original Erdős–Hajnal problem list gives the additional conditions $\gamma \ge 2$, $r<\omega$, and ${\kappa }_{\alpha }>r$. Without $\gamma \ge 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$.

Source and licence

Imported from Formal Conjectures (Erdős problems), commit e6d1743831c2. Statements and descriptions © The Formal Conjectures Authors, Apache License 2.0; reformatted for this page.