A Nonuniversality Obstruction to an Ordinal Graph Partition Relation
Overview
Erdős #597 asks which graphs must appear in two-colorings of the ordinal square ω₁². This note applies Shelah's known nonuniversality theorem to Baumgartner's negative partition relation as reported by Erdős, giving a counterexample to the unrestricted infinite-target assertion. The target has exactly ℵ₁ vertices, is connected and bipartite, has diameter at most three, and contains no countably infinite complete bipartite graph. An explicit biclique-rank proof and connected target accompany the application; Shelah's prior tree-comparability mechanism is credited. The Lean companion verifies the construction and deduction from the cited Baumgartner theorem, whose proof lies outside the codebase; Reference-Gated names this machine-verification boundary. The finite-target question remains open.
Original public questions
Erdős #597: the unrestricted infinite-target assertion
Paul Erdős: Some problems on finite and infinite graphs (1987) — Printed p.224: the forbidden-K4 and forbidden-countable-biclique graph question, the reported Baumgartner relation, and the separately posed finite-target variant.
Erdős Problems: problem 597 — The result addresses the unrestricted infinite-target assertion; it does not settle the finite-target question or claim endorsement by the problem-list maintainer.
Original abstract (English)
Erdős Problem 597 asks whether every graph on at most ℵ₁ vertices omitting both a four-vertex clique and a countably infinite complete bipartite graph is forced as a blue subgraph in every colouring of the ordinal square ω₁² with no red homogeneous set of order type ω₁·ω. We identify a nonuniversality obstruction to this assertion: applying Shelah's theorem for graphs omitting the countable biclique to Baumgartner's negative partition relation, as recorded by Erdős, gives a negative answer to this unrestricted assertion. The obstructing target can have exactly ℵ₁ vertices and be connected and bipartite, with diameter at most three. We give an elementary well-founded-tree proof of the required special case of Shelah's nonuniversality theorem. The separate question about finite target graphs remains unresolved by this argument.
Mathematical review
The machine-checked deduction uses the documented cited theorems as inputs. Their proofs are outside the current code package. Complete formalization must also include checked proofs of those cited results.
Review standard