← All topics
Proposition

Two axioms, one idea

The domino principle and 'there is always a smallest one' are secretly the same fact in different clothes.
Formally: Induction and well-ordering are inter-derivablelogic foundationsTakes focusdepth 1 in the graph

Induction and well-ordering look unrelated — one is about climbing up, the other about a floor at the bottom. But each can be proved from the other: if you couldn't induct, there'd be a smallest failure; if there were a floorless descending set, induction would break. Mathematics is full of these equivalences, and recording them as explicit graph edges is exactly what Ouroboros is for.

Two doors into the same room. Whichever you walk through, you end up with the same power over the natural numbers.

From well-ordering, prove induction: suppose P(0) holds and P(n) implies P(n+1), yet P fails somewhere. The set of failures has a least element m. m isn't 0, so P(m-1) holds... but then P(m) holds. Contradiction.

Knowing two principles are equivalent means you can use whichever is more convenient — and trust nothing is lost. Equivalence edges like this are how the knowledge graph exposes hidden structure.

Level 1 The precise statement

Over the natural numbers the Axiom of Induction and the Well-Ordering Principle are logically equivalent: each can be derived from the other.

Level 2 The proof
WO => induction: if the set of counterexamples to P were nonempty it would have a least element m > 0, but P(m-1) then forces P(m), a contradiction. Induction => WO: a nonempty set with no least element can be shown empty by induction on membership below n.
Level 3 What it stands on (2 direct)
Level 4 The verified record

This page is generated from a machine-checked node. The kernel confirms its dependencies resolve, nothing is circular, and it grounds in axioms (foundation: peano). The content hash below makes tampering evident.

sha256:0f9bdb51989e2c268d372f813d62e073cf3217b2c518f2f8060b3a494fcb45db

Nothing yet — this is a frontier result.

Nothing depends on it yet, so its failure would be contained.

🔬 Open in the workbench🎓 More topics