Erdős Problem #1220 in Lean 4: the affirmative statement is not provable in ZFC
Erdős problem #1220 (erdosproblems.com/1220; Erdős–Hajnal 1971): let λ be a singular cardinal such that both λ and cf(λ) are ℵ₀-inaccessible (μ^ℵ₀ < κ for all μ < κ); does λ → (λ, ℵ₁)² hold? This formalization settles the question as asked on erdosproblems.com in the negative sense "not provable": ZFC does not prove that every such λ satisfies λ → (λ, ℵ₁)² (erdos1220_not_provable : ¬ (ZFC ⊨ᵇ Erdos1220)), i.e. there is a model of ZFC with a singular λ, λ and cf(λ) ℵ₀-inaccessible, and λ ↛ (λ, ℵ₁)². Shelah and Stanley (Sh:258, Ann. Pure Appl. Logic 36 (1987)) showed that a negative answer is…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-26-000001
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-26-000001/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-26-000001/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'