How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Erdős–Rado for arbitrary infinite cardinals and finite arity
Statement
In ZFC, for every infinite cardinal and every ,
Here is cardinal successor and . In particular the theorem includes .
Facts & Assumptions
Given: An infinite cardinal ; assume AC.
Relative beths satisfy and . Finite beth iteration above an infinite cardinal
Pattern closure for , , positive finite and domain gives distinct () and an outside point whose patterns on earlier nodes agree with those of each . Pattern closure yields an end-homogeneous sequence
An infinite cardinal times itself equals itself. Absorption: for cardinals with infinite and , , and when
Natural-number induction proves the assertion from zero and successor cases. The principle of mathematical induction
The arrow means every coloring has a homogeneous subset of the target cardinality. Partition arrows and homogeneous sets
Cantor's theorem gives for every infinite cardinal . Cantor's theorem:
Assume AC. The Axiom of Choice
Proof
For , let . If every color fiber had size less than , each would have size at most by the successor-cardinal definition. AC chooses an injection of each fiber into , giving an injection of their union into by recording the color and its fiber index. F3 bounds the union by , contrary to its size . Therefore some fiber has size and is homogeneous. By F1 this is exactly the required zero case.
Assume the assertion at , and let . Put . Repeatedly applying F6 to the recurrence F1 gives and infinite. Thus F2 applies with , and . Obtain distinct nodes for and outside their range.
Define by . The argument has size because the are distinct and is outside their range, so is well-defined. The induction assertion at , with , gives of size homogeneous for , of some color .
Put ; injectivity gives . For any nodes of , order their indices as and put . These are previous nodes at stage , so F2 gives . Hence is homogeneous. Only the largest index was used; no ambient increase of the was assumed. This proves the successor step; F4 and step 1.1 prove all finite .
Depends on
- Finite beth iteration above an infinite cardinal
- Pattern closure yields an end-homogeneous sequence
- Absorption: for cardinals $\kappa, \lambda$ with $\kappa$ infinite and $\lambda \le \kappa$, $\kappa \oplus \lambda = \kappa$, and $\kappa \otimes \lambda = \kappa$ when $\lambda \ne 0$
- The principle of mathematical induction
- Partition arrows and homogeneous sets
- Cantor's theorem: $A \prec \mathcal{P}(A)$
- The Axiom of Choice
Used by
Dependency tree · two levels
27 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.