Skip to content

Erdős problem 1128

Erdős Problem 1128 (disproved by Prikry–Mills, 1978):

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

1128.lean

Retained formal statement4 of 4

The claim that every 2-colouring of ω1×ω1\omega_1 \times \omega_1 has an uncountable monochromatic product rectangle is false in ZFC.

Counterexample: The ordering colouring f(α,β)=0f(\alpha, \beta) = 0 iff α<β\alpha < \beta has no uncountable monochromatic product rectangle A1×B1A_1 \times B_1.

Proof: If A1×B1A_1 \times B_1 were monochromatic with colour 0, then every element of A1A_1 would be strictly less than every element of B1B_1, making A1A_1 bounded above in ω1\omega_1; but any bounded subset of ω1\omega_1 is countable (since initial segments are countable), contradicting A1A_1 being uncountable. The colour-1 case is symmetric with the roles of A1A_1 and B1B_1 swapped.

Note: The correct classical result for 2-colourings of pairs (not products) is the Erdős–Rado theorem ω1→(ω1)22\omega_1 \to (\omega_1)^2_2, which concerns unordered pairs.

FormalConjectures/ErdosProblems/1128.leanErdos1128.erdos_1128.variants.two_dimensional_false2 linesExact file
¬∀ (f : Erdos1128.Omega1✝ → Erdos1128.Omega1✝ → Fin 2),    ∃ A₁ B₁, ¬A₁.Countable ∧ ¬B₁.Countable ∧ ∃ c, ∀ a ∈ A₁, ∀ b ∈ B₁, f a b = c
SolvedStatement only, no proof