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.
Two finite disjoint petals can be made cross-incomparable
Statement
In ZFC, if is an Aronszajn tree and is an uncountable family of pairwise disjoint finite subsets of , then distinct satisfy: every node in is incomparable with every node in .
Facts & Assumptions
Given: Such and ; assume AC. Here a family is a set of distinct finite subsets, and “comparable” includes equality.
Aronszajn trees have height , countable levels and no cofinal branch. Aronszajn, Suslin and special trees
On every uncountable set there is an ultrafilter all of whose members are uncountable and containing every cocountable subset. An ultrafilter containing all cocountable subsets
If a finite union belongs to an ultrafilter, one of its terms belongs to it. Ultrafilters are prime: a union in has a member in
Nodes with a common tree extension are comparable, and strict tree order strictly increases height; predecessors at a specified smaller height are unique. Tree predecessors and compatibility
Countable unions of countable sets are countable under countable choice. Countable unions of at most countable sets, assuming
Filters are closed under pairwise intersections, omit the empty set, and are upward closed. Filter on a set
Assume AC. The Axiom of Choice
Proof
If , pair it with any other member; the conclusion is vacuous and there is another member because is uncountable. Otherwise every member has positive size. Partition by its finite sizes. F5 and A1 imply that some size occurs uncountably often; restrict to that subfamily, still denoted . Use AC to fix for each an enumeration .
Fix an ultrafilter on as in F2. Suppose the conclusion fails. For and let . For fixed , failure supplies a comparable pair between and every , so the finite union of over contains . This cocountable set belongs to , and upward closure F6 puts the union in . F3 gives a pair with and . Use the already fixed finite enumeration and the usual order on to take its first such pair.
Some occurs as on an uncountable subfamily : otherwise its finitely many fibers would all be countable and F5 would make countable. For distinct , F6 gives , so F2 says is uncountable. Put . The set is countable by F1 and F5, since is countable. The map is injective on because its members are disjoint. Consequently only countably many can have . Choose an outside those exceptions. Its th node is comparable with and strictly higher than both, so F4 forces it to extend both. Hence are comparable.
The set is therefore an uncountable chain: injectivity follows from disjointness, and comparability from step 3.1. Its heights are unbounded in , since any bounded collection of levels is countable by the same F1/F5 argument. Its downward closure is a chain: compare two witnesses in and use F4 to compare both predecessors below the higher witness. It is cofinal. It is also maximal: if a node is comparable with every member of , take of height above ; F4 forces , whence . Thus is a cofinal branch, contradicting F1. The failure assumed in step 2.1 is impossible, proving the assertion.
Depends on
- Aronszajn, Suslin and special trees
- An ultrafilter containing all cocountable subsets
- Ultrafilters are prime: a union in $\mathcal{U}$ has a member in $\mathcal{U}$
- Tree predecessors and compatibility
- Countable unions of at most countable sets, assuming $\mathrm{AC}_\omega$
- Filter on a set
- The Axiom of Choice
Used by
Dependency tree · two levels
28 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.