Erdős Problem #70

The question

erdos_70. Erdős Problem 70: Let $\mathfrak{c}$ be the order type of the real numbers, let $\beta$ be a countable ordinal, and let $2\le n<\omega$. Is it true that $\mathfrak{c}\to (\beta ,n{)}_2^3$?

Note: The cases $n\le 3$ are trivially true (compare omega_three), so the genuine content of the conjecture begins at $n=4$.

omega_times_two_four. First open case beyond Erdős–Rado: $\mathfrak{c}\to (\omega \cdot 2,4{)}_2^3$, where $\mathfrak{c}$ is the order type of the real numbers.

Erdős and Rado proved $\mathfrak{c}\to (\omega +n,4{)}_2^3$ for every finite $n\ge 2$ (see erdos_rado), which covers all red ordinals below $\omega \cdot 2=\omega +\omega$. This variant asks whether the result extends to $\beta =\omega \cdot 2$, the simplest countable ordinal not covered by their theorem.

omega_one. The relation at ${\omega }_1$: $\mathfrak{c}\to ({\omega }_1,n{)}_2^3$ for finite $n\ge 2$, where ${\omega }_1={\aleph }_1$ is the first uncountable ordinal.

Note that ${\omega }_1$ is not a countable ordinal, so this is not directly an instance of the main Erdős problem (which asks for countable $\beta$). Under CH, ${\omega }_1=\mathfrak{c}.\mathrm{ord}$, making this a self-referential question about $\mathfrak{c}.\mathrm{ord} \to (\mathfrak{c}.\mathrm{ord}, n)^3_2$.

Formal statement (Lean 4)

From Formal Conjectures, module FormalConjectures.ErdosProblems.«70» (3 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_70 :
    answer(sorry) ↔
    ∀ᵉ (β : Ordinal.{0}) (n : ℕ) (_ : β.card ≤ ℵ₀) (_ : 2 ≤ n),
      RealCardinalRamsey3 β n

theorem omega_times_two_four :
    answer(sorry) ↔ RealCardinalRamsey3 (ω * 2) 4

theorem omega_one :
    answer(sorry) ↔
    ∀ᵉ (n : ℕ) (_ : 2 ≤ n),
      OrdinalCardinalRamsey3 (𝔠).ord (Cardinal.aleph 1).ord n

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/70. Report it as a literature claim.
• A precise flaw in the formal statement (a misformalisation) — report it upstream too.

References

• erdosproblems.com/70
• [ErRa56] Erdős, P. and Rado, R., A partition calculus in set theory, Bull. Amer. Math. Soc. 62 (1956), 427–489, Theorem 31.
• [Er87] Erdős, P., Some problems on finite and infinite graphs, Logic and combinatorics (Arcata, Calif., 1985), Contemp. Math. 65 (1987), 223–228.

The 3-uniform (triple) partition relation $\mathfrak{c}\to (\beta ,n{)}_2^3$, where $\mathfrak{c}$ denotes the order type of the real numbers with their usual order (written $\lambda$ in [ErRa56]). This is the triple analogue of OrdinalCardinalRamsey used in Problems 590–592; the file also contains the analogous relation for an ordinal in place of the real line.

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.