Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passverified 2026-08-02 (claude-opus-5)
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.

Categoricity: the natural numbers are unique up to unique isomorphism

Statement

Let (N,0,σ)(N, 0, \sigma) and (N′,0′,σ′)(N', 0', \sigma') be Peano systems (Peano system). There is a unique bijection h:N→N′h : N \to N' with h(0)=0′h(0) = 0' and h(σ(n))=σ′(h(n))h(\sigma(n)) = \sigma'(h(n)) for all n∈Nn \in N, an isomorphism of Peano systems. Thus the natural numbers are determined up to a unique isomorphism.

Facts & Assumptions

Given: Two Peano systems (N,0,σ)(N, 0, \sigma) and (N′,0′,σ′)(N', 0', \sigma').

[L1]

Recursion theorem, valid in any Peano system since its proof uses only the axioms P1 to P3: for a set AA, an element a∈Aa \in A, and f:A→Af : A \to A, there is a unique g:N→Ag : N \to A with g(0)=ag(0) = a and g(σ(n))=f(g(n))g(\sigma(n)) = f(g(n)) (The recursion theorem).

[L2]

Induction holds in each system (axiom P3): a subset containing the base point and closed under the successor is the whole system (Peano system).

Proof

technique · direct
1.1

Apply the recursion theorem [L1] in (N,0,σ)(N, 0, \sigma) with A=N′A = N', a=0′a = 0', f=σ′f = \sigma': there is a unique h:N→N′h : N \to N' with h(0)=0′h(0) = 0' and h(σ(n))=σ′(h(n))h(\sigma(n)) = \sigma'(h(n)).

L1
1.2

Symmetrically, apply [L1] in (N′,0′,σ′)(N', 0', \sigma') with A=NA = N, a=0a = 0, f=σf = \sigma: there is a unique h′:N′→Nh' : N' \to N with h′(0′)=0h'(0') = 0 and h′(σ′(n′))=σ(h′(n′))h'(\sigma'(n')) = \sigma(h'(n')).

L1
2.1

The composite h′∘h:N→Nh' \circ h : N \to N satisfies (h′∘h)(0)=h′(0′)=0(h' \circ h)(0) = h'(0') = 0 and (h′∘h)(σ(n))=h′(σ′(h(n)))=σ(h′(h(n)))=σ((h′∘h)(n))(h' \circ h)(\sigma(n)) = h'(\sigma'(h(n))) = \sigma(h'(h(n))) = \sigma((h' \circ h)(n)); the identity idN\mathrm{id}_N satisfies the same two equations, so by induction [L2] the set { n:(h′∘h)(n)=n }\{\, n : (h' \circ h)(n) = n \,\} is all of NN, i.e. h′∘h=idNh' \circ h = \mathrm{id}_N.

step 1.1step 1.2L2
2.2

Likewise h∘h′=idN′h \circ h' = \mathrm{id}_{N'} by the same argument carried out in N′N'.

step 1.1step 1.2L2
3.1

Hence hh is a bijection with inverse h′h', and it preserves the base point and the successor, so it is an isomorphism of Peano systems.

step 2.1step 2.2
4.1

Uniqueness: any h1:N→N′h_1 : N \to N' with h1(0)=0′h_1(0) = 0' and h1(σ(n))=σ′(h1(n))h_1(\sigma(n)) = \sigma'(h_1(n)) satisfies the recursion clauses defining hh in step 1.1, so h1=hh_1 = h by the uniqueness in [L1] (equivalently { n:h1(n)=h(n) }\{\, n : h_1(n) = h(n) \,\} contains 00 and is closed under σ\sigma, hence is all of NN by induction [L2]).

step 1.1L1L2∎

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: 19 results over 11 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