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.
Prescribed-start and starting-point-free serial choice are equivalent in ZF
Statement
In ZF, the starting-point-free and prescribed-start global principles in The serial-relation Dependent Choice principle over ZF are equivalent.
Facts & Assumptions
Given: ZF and the two global principles in the statement.
Starting-point-free DC supplies a chain on any nonempty serial carrier; prescribed-start DC also fixes its initial value (The serial-relation Dependent Choice principle over ZF).
Separation forms a subset specified by a formula with parameters (The Axiom Schema of Separation: for each formula , ).
Replacement forms the image of a set under a uniquely specified assignment (The Axiom Schema of Replacement: for each formula , if defines a class function on then its image on is a set).
The union of a set has precisely the elements belonging to its members (The union of a set, and the binary union ).
A property holding at zero and preserved by successor holds on all naturals (The principle of mathematical induction).
Proof
Assume prescribed-start DC. Given nonempty and serial , fix one . Its prescribed chain is a chain with unrestricted start, so starting-point-free DC follows. This is a single existential instantiation, not a family of selections.
Conversely assume starting-point-free DC, and fix nonempty , serial and . By Separation in , the pairs with , , , and for every form a set . The pair belongs to , since there are no adjacent coordinates to check.
Define on by exactly when extends . This is a subset of . For any , seriality gives one with ; the function has domain and satisfies all required edges, old ones from and the new last edge by the choice of . Thus is serial. No simultaneous successor function has been selected.
Apply starting-point-free DC to the nonempty set and serial . It gives with extending and . Induction gives and, for , : the zero case is reflexivity, and each successor uses one end extension. In particular the domains are unbounded in .
Replacement gives the set and Union gives . Two pairs in with the same first coordinate lie together in , so have the same second coordinate. Every lies in , since , and all domains lie in . Consequently and .
For any , both and lie in . That path's edge gives . Hence is the prescribed chain. Together with the first implication this proves the equivalence, without any additional choice axiom.
Depends on
The serial-relation Dependent Choice principle over ZF
The principle of mathematical induction
The recursion theorem
The set of all functions
The Axiom Schema of Separation: for each formula ,
The Axiom Schema of Replacement: for each formula , if defines a class function on then its image on is a set
The union of a set, and the binary union