Lecture IV (§4) — Definition 4.5 and Theorem 4.6: models of Peano's Axioms

Following Dana Scott, Lectures on a Mathematical Theory of Computation, PRG-19 (1981), Lecture IV, Fixed points and recursion, pages 65–66.

• Definition 4.5 — a model for Peano's Axioms is a structured set ⟨N, 0, ⁺⟩ (a type N with a distinguished element 0 : N and a unary successor ⁺ : N → N) satisfying: (i) 0 ≠ n⁺ for all n; (ii) n⁺ = m⁺ ⟹ n = m (the successor is injective); (iii) induction: whenever x ⊆ N has 0 ∈ x and x⁺ ⊆ x, then x = N. We package this as PeanoModel, stating (iii) in the equivalent point form 0 ∈ s → (∀ n ∈ s, n⁺ ∈ s) → ∀ n, n ∈ s (x⁺ ⊆ x is ∀ n ∈ x, n⁺ ∈ x; x = N is ∀ n, n ∈ x).

• Theorem 4.6 — all models of Peano's Axioms are isomorphic (peano_models_isomorphic). Scott's proof is an application of the Fixed-point Theorem 4.1: between models ⟨N,0,⁺⟩ and ⟨M,□,#⟩ he forms, on the powerset domain P(N × M), the approximable operator u ↦ {(0,□)} ∪ {(n⁺,m#) ∣ (n,m) ∈ u} and takes its least fixed point r.

  We realize that least fixed point directly as the inductively generated relation Graph (the least set of pairs containing (0,□) and closed under (n,m) ↦ (n⁺,m#) — exactly the least fixed point of Scott's monotone operator, by Theorem 4.1). Scott's two facts (i) 0 r □ and (ii) n r m ⟹ n⁺ r m# are the two constructors. We then show Graph is a one-one correspondence: functionality + totality on the right (exists_unique_right, by induction 4.5(iii) using 4.5(i)/(ii) to invert the generating rules) and, by the symmetry of the construction, on the left (exists_unique_left). This yields the structure-preserving bijection e : N ≃ M with e 0 = □ and e (n⁺) = (e n)#.

All of the content (the relation Graph, the uniqueness lemmas) is choice-free (#print axioms ⊆ {propext, Quot.sound}); only the packaging of the bijection N ≃ M from the functional-and-total relation pulls Classical.choice, exactly as a Dedekind/recursion theorem must.

structure Domain.Neighborhood.PeanoModel (N : Type u) : Type u

Definition 4.5 (Scott 1981, PRG-19). A model for Peano's Axioms: a type N with a distinguished element zero and a unary successor, satisfying

• (i) zero ≠ succ n for all n (zero_ne_succ);
• (ii) succ is injective (n⁺ = m⁺ ⟹ n = m) (succ_injective);
• (iii) mathematical induction: any s ⊆ N with zero ∈ s and closed under succ (∀ n ∈ s, succ n ∈ s, i.e. Scott's x⁺ ⊆ x) is all of N (∀ n, n ∈ s, i.e. Scott's x = N) (induction).

• zero : N

  The distinguished zero 0 ∈ N.

• succ : N → N

  The unary successor ⁺ : N → N.

• zero_ne_succ (n : N) : self.zero ≠ self.succ n

  4.5(i) 0 ≠ n⁺.

• succ_injective : Function.Injective self.succ

  4.5(ii) the successor is one-one.

• induction (s : Set N) : self.zero ∈ s → (∀ (n : N), n ∈ s → self.succ n ∈ s) → ∀ (n : N), n ∈ s

  4.5(iii) the induction principle (point form of x⁺ ⊆ x ⟹ x = N).

inductive Domain.Neighborhood.PeanoModel.Graph {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) : M → N → Prop

Scott's least fixed point r ⊆ N × M, realized as the inductively generated relation: the least relation containing (0, □) and closed under (n, m) ↦ (n⁺, m#). The two constructors are Scott's facts (i) 0 r □ and (ii) n r m ⟹ n⁺ r m#. By Theorem 4.1 this is the least fixed point of the approximable operator u ↦ {(0,□)} ∪ {(n⁺,m#) ∣ (n,m) ∈ u} on P(N × M).

• base {M : Type u} {N : Type v} {P : PeanoModel M} {Q : PeanoModel N} : P.Graph Q P.zero Q.zero
• step {M : Type u} {N : Type v} {P : PeanoModel M} {Q : PeanoModel N} {m : M} {n : N} : P.Graph Q m n → P.Graph Q (P.succ m) (Q.succ n)

theorem Domain.Neighborhood.PeanoModel.Graph.swap {M : Type u} {N : Type v} {P : PeanoModel M} {Q : PeanoModel N} {m : M} {n : N} (h : P.Graph Q m n) : Q.Graph P n m

The construction is symmetric in the two models: Graph P Q m n swaps to Graph Q P n m. (This is why the relation is one-one in both directions, as Scott notes: "the rôles of N and M are completely symmetric".)

theorem Domain.Neighborhood.PeanoModel.graph_zero_right {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) {k : N} (h : P.Graph Q P.zero k) : k = Q.zero

Inversion at 0 (uses 4.5(i)). Anything related to 0 on the left is □ on the right: 0 r k ⟹ k = □. (The other generating rule would force 0 = n⁺, impossible by 4.5(i).)

theorem Domain.Neighborhood.PeanoModel.graph_succ_right {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) {m : M} {k : N} (h : P.Graph Q (P.succ m) k) : ∃ (n : N), P.Graph Q m n ∧ k = Q.succ n

Inversion at a successor (uses 4.5(i)/(ii)). Anything related to n⁺ on the left comes from a relation n r n₀ with right value a successor: n⁺ r k ⟹ ∃ n₀, n r n₀ ∧ k = n₀#.

theorem Domain.Neighborhood.PeanoModel.exists_unique_right {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) (m : M) : ∃! n : N, P.Graph Q m n

Each element of the left model is related by Graph to exactly one element of the right model. Proved by the induction principle 4.5(iii) on the set {m ∣ ∃! n, m r n}: the base case is the 0-inversion graph_zero_right, the step case the successor-inversion graph_succ_right together with 4.5(ii).

theorem Domain.Neighborhood.PeanoModel.exists_unique_left {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) (n : N) : ∃! m : M, P.Graph Q m n

Dually (by Graph.swap), each element of the right model is related to exactly one element of the left model.

theorem Domain.Neighborhood.PeanoModel.peano_models_isomorphic {M : Type u} {N : Type v} (P : PeanoModel M) (Q : PeanoModel N) : ∃ (e : M ≃ N), e P.zero = Q.zero ∧ ∀ (m : M), e (P.succ m) = Q.succ (e m)

Theorem 4.6 (Scott 1981, PRG-19). All models of Peano's Axioms are isomorphic. Between any two models there is a bijection e : N ≃ M of the underlying sets that preserves the structure: e 0 = □ and e (n⁺) = (e n)#. The bijection is the least-fixed-point relation Graph, which exists_unique_right/exists_unique_left show is a one-one correspondence; the two structure equations are the constructors Graph.base/Graph.step.