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.
Injectivity of the successor is independent of the other Peano axioms
Statement refuted
Refuted claim: (P2) injectivity of follows from (P1) is not a successor together with (P3) induction. The witness is the three-element system with , , .
Facts & Assumptions
Given: , base point , , , .
The Peano axioms (Peano system).
Counterexample
P1 holds: the values of are , , , none of which is , so for all .
P3 holds: if with and closed under , then forces , then , so ; thus induction holds.
P2 fails: but , so is not injective.
So satisfies P1 and P3 but not P2, refuting the claim; note the failure permits the pathology (a number that is its own successor) and a finite model in which distinct numerals collapse.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 10 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Peano axioms (Wikipedia) (standard reference, not scraped)
- Mathematical induction (Wikipedia) (standard reference, not scraped)
- Peano axioms (Encyclopedia of Mathematics) (standard reference, not scraped)