Exercise 4.22 (Scott 1981, PRG-19, Lecture IV) — carving a Peano model out of a

partial one

Suppose N* is a structured set ⟨N*, 0, ⁺⟩ satisfying only axioms (i) and (ii) of Definition 4.5 — i.e. 0 ≠ n⁺ (zero is not a successor) and ⁺ is injective — but not necessarily the induction axiom (iii). Must there be a subset N ⊆ N* that satisfies (i), (ii), and (iii)?

Yes. Following Scott's hint, take the least fixed point in P(N*) (Exercise 4.14 / 4.13(2), the dual Knaster–Tarski over the complete lattice P(N*)) of the monotone operator

g(x) = {0} ∪ x⁺ = {0} ∪ {n⁺ ∣ n ∈ x}.

This least fixed point nats is the smallest subset of N* containing 0 and closed under ⁺ (zero_mem_nats, succ_mem_nats). On the subtype N = {m // m ∈ nats}:

• (i) 0 ≠ n⁺ and (ii) ⁺ injective are inherited from N*;
• (iii) induction holds by minimality of the least fixed point: a subset of N closed under 0/⁺ pulls back to a pre-fixed point of g in P(N*), which therefore contains nats.

So ⟨N, 0, ⁺⟩ is a genuine model of Peano's Axioms (peanoSub), giving exists_peano_submodel.

(For set theorists.) The existence of such an N* at all is guaranteed by the axiom of infinity: the standard ⟨ℕ, 0, ⁺⟩ is one (PeanoModel ℕ, recorded as natPeano), and indeed it already satisfies (iii), so it is its own carved-out model.

The subset nats is built choice-free (lfpSet); the PeanoModel packaging of peanoSub and the existence statement live over Classical.choice exactly as Theorem 4.6's bijection does.

def Domain.Neighborhood.Exercise422.genOp {M : Type u_1} (zero : M) (succ : M → M) (x : Set M) : Set M

Scott's operator g(x) = {0} ∪ x⁺ on P(N*), whose least fixed point is the smallest subset containing 0 and closed under the successor.

Equations

• Domain.Neighborhood.Exercise422.genOp zero succ x = {zero} ∪ succ '' x

theorem Domain.Neighborhood.Exercise422.genOp_monotone {M : Type u_1} (zero : M) (succ : M → M) : Monotone (genOp zero succ)

def Domain.Neighborhood.Exercise422.nats {M : Type u_1} (zero : M) (succ : M → M) : Set M

The carved-out subset N ⊆ N*: the least fixed point of g (Exercise 4.13(2)/4.14).

Equations

• Domain.Neighborhood.Exercise422.nats zero succ = Domain.Neighborhood.Exercise414.lfpSet (Domain.Neighborhood.Exercise422.genOp zero succ)

theorem Domain.Neighborhood.Exercise422.genOp_nats {M : Type u_1} (zero : M) (succ : M → M) : genOp zero succ (nats zero succ) = nats zero succ

theorem Domain.Neighborhood.Exercise422.zero_mem_nats {M : Type u_1} (zero : M) (succ : M → M) : zero ∈ nats zero succ

0 ∈ N — directly from the lfpSet definition (no monotonicity needed), keeping the construction choice-free.

theorem Domain.Neighborhood.Exercise422.succ_mem_nats {M : Type u_1} (zero : M) (succ : M → M) {n : M} (hn : n ∈ nats zero succ) : succ n ∈ nats zero succ

N is closed under the successor: n ∈ N ⟹ n⁺ ∈ N — again directly from lfpSet.

theorem Domain.Neighborhood.Exercise422.nats_induction {M : Type u_1} (zero : M) (succ : M → M) (s : Set M) (h0 : zero ∈ s) (hsucc : ∀ (n : M), n ∈ s → succ n ∈ s) : nats zero succ ⊆ s

Induction by minimality. Any subset s ⊆ N* containing 0 and closed under ⁺ contains all of N. (This is the heart of axiom (iii): s is a pre-fixed point of g, hence dominates the least fixed point nats.)

The carved-out structure is a model of Peano's Axioms.

@[reducible, inline]

abbrev Domain.Neighborhood.Exercise422.Nat' {M : Type u_1} (zero : M) (succ : M → M) : Type u_1

The subtype N = {m // m ∈ nats} carrying the carved-out Peano structure.

Equations

• Domain.Neighborhood.Exercise422.Nat' zero succ = { m : M // m ∈ Domain.Neighborhood.Exercise422.nats zero succ }

def Domain.Neighborhood.Exercise422.subZero {M : Type u_1} (zero : M) (succ : M → M) : Nat' zero succ

The zero of the subtype.

Equations

• Domain.Neighborhood.Exercise422.subZero zero succ = ⟨zero, ⋯⟩

def Domain.Neighborhood.Exercise422.subSucc {M : Type u_1} (zero : M) (succ : M → M) (n : Nat' zero succ) : Nat' zero succ

The successor of the subtype (well-defined by closure succ_mem_nats).

Equations

• Domain.Neighborhood.Exercise422.subSucc zero succ n = ⟨succ ↑n, ⋯⟩

def Domain.Neighborhood.Exercise422.peanoSub {M : Type u_1} (zero : M) (succ : M → M) (hzero : ∀ (n : M), zero ≠ succ n) (hinj : Function.Injective succ) : PeanoModel (Nat' zero succ)

Exercise 4.22 (Scott 1981, PRG-19). The carved-out subset N ⊆ N*, with the inherited 0 and ⁺, is a model of all three Peano axioms — even though N* was only assumed to satisfy (i) and (ii). Axioms (i)/(ii) are inherited; (iii) holds by minimality of the least fixed point.

Equations

• One or more equations did not get rendered due to their size.

theorem Domain.Neighborhood.Exercise422.exists_peano_submodel {M : Type u_1} (zero : M) (succ : M → M) (hzero : ∀ (n : M), zero ≠ succ n) (hinj : Function.Injective succ) : Nonempty (PeanoModel (Nat' zero succ))

Exercise 4.22 (Scott 1981, PRG-19). Yes: whenever N* satisfies (i) and (ii), there is a subset N ⊆ N* (carrying the inherited structure) satisfying (i), (ii), and (iii).

Existence of N* (axiom of infinity): the standard ℕ.

def Domain.Neighborhood.Exercise422.natPeano : PeanoModel ℕ

(For set theorists.) The standard natural numbers ⟨ℕ, 0, ⁺⟩ form a model of Peano's Axioms; their existence is the axiom of infinity. (This witnesses that an N* satisfying (i)/(ii) — in fact all three — exists in the first place.)

Equations

• One or more equations did not get rendered due to their size.