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.
Branches through countable normal trees of limit height
Statement
If is countable and normal of nonzero countable limit height , every node lies on a branch cofinal in . There is a countable collection of such branches covering . The construction works in ZF, with no use of Choice.
Facts & Assumptions
Given: Such and , and an arbitrary .
Normality gives an extension at every strictly higher level below the tree height. Normal and splitting trees
Natural-number recursion defines the unique orbit of a function on a set from a specified initial state. The recursion theorem
Every node has a unique predecessor of every smaller height, and two predecessors of a common node are comparable. Strict order increases height. Tree predecessors and compatibility
Proof
Fix surjections and . They exist by countability: is infinite, and has nodes at arbitrarily high levels below , so it too is infinite. Only these two witnesses are fixed. Define and . The successor of every ordinal below the limit is still below , so recursion gives a strictly increasing sequence in . It is cofinal since . The nonautonomous rule is a recursion on the state .
Starting at , let and take for the least for which and . The candidate set is nonempty by normality. Recursion on supplies this sequence, and its heights are cofinal because . Least natural indices require no choice function.
Put . It contains and is a chain: if and , both lie below , so they are comparable. Its heights are cofinal by step 2.1.
If can be adjoined to while retaining a chain, choose with , possible by cofinality and the limit-height hypothesis. Comparability with and strict increase of height force , hence . Thus is maximal and is a cofinal branch.
The same fixed determine uniquely for each . Replacement therefore forms . The sequence is onto , so it is countable, and proves that it covers . The construction includes the root and every prescribed node; no last level exists at the limit height.
Depends on
Used by
Dependency tree · two levels
7 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.
Sources
- Karagila, Axiomatic Set Theory, Lemma 9.11 and its proof, printed p45 (branch existence expanded locally) (standard reference, not scraped)