Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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,σ) and (N′,0′,σ′) be Peano systems (Peano system). There is a unique bijection h:N→N′ with h(0)=0′ and h(σ(n))=σ′(h(n)) for all n∈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,σ) and (N′,0′,σ′).

[L1]

Recursion theorem, valid in any Peano system since its proof uses only the axioms P1 to P3: for a set A, an element a∈A, and f:A→A, there is a unique g:N→A with g(0)=a and g(σ(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.1L1

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

1.2L1

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

2.1step 1.1step 1.2L2

The composite h′∘h:N→N satisfies (h′∘h)(0)=h′(0′)=0 and (h′∘h)(σ(n))=h′(σ′(h(n)))=σ(h′(h(n)))=σ((h′∘h)(n)); the identity idN satisfies the same two equations, so by induction [L2] the set { n:(h′∘h)(n)=n } is all of N, i.e. h′∘h=idN.

2.2step 1.1step 1.2L2

Likewise h∘h′=idN′ by the same argument carried out in N′.

3.1step 2.1step 2.2

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

4.1step 1.1L1L2∎

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

Depends on

Dependency tree · 2 levels

Sources