Exercise 4.21 (Scott 1981, PRG-19, Lecture IV) — ≤ as a unique fixed point;

addition & multiplication

Scott asks to show that the less-than-or-equal-to relation ℓ ⊆ ℕ × ℕ is uniquely determined by the fixed-point equation

ℓ = {(n, n) ∣ n ∈ ℕ} ∪ {(n, m⁺) ∣ (n, m) ∈ ℓ}.

Working in the power-set domain P(ℕ × ℕ) (a complete lattice, Exercise 4.14), the right-hand side is a monotone operator leOp. We show:

• leRel = {(n, m) ∣ n ≤ m} solves the equation (leRel_isFixed);
• the solution is unique (leOp_unique): for any fixed point u one proves, by induction on the second coordinate, that (n, m) ∈ u ↔ n ≤ m. (Unlike a general least-fixed-point situation, here the equation pins the relation down completely, because the clause (n, m⁺) never produces a pair with second coordinate 0.)

Scott then considers ⟨P ℕ, ℕ, ⁺⟩ with x⁺ = {n⁺ ∣ n ∈ x} and the unique function [·] : ℕ → P ℕ of 4.13(3) determined by [0] = ℕ and [m⁺] = [m]⁺. We identify it as the up-set [m] = {k ∣ m ≤ k} (upSet), with upSet_zero/upSet_succ the two recursion equations and upSet_unique their uniqueness (4.13(3)).

The structures ⟨ℕ, 0, ⁺⟩ and ⟨[m], m, ⁺⟩ are uniquely isomorphic via n ↦ m + n (addIso), connecting the isomorphism with ordinary addition (addIso_apply): the unique structure-preserving bijection sends n to m + n.

Finally, multiplication: the hint equation n·ℕ = {0} ∪ {n + m ∣ m ∈ n·ℕ} has, as its least solution in P ℕ, exactly the set of multiples of n (mulOp_lfp_eq_multiples).

All set-level constructions are choice-free (#print axioms ⊆ {propext, Quot.sound}).

The order relation as a unique fixed point.

def Domain.Neighborhood.Exercise421.leOp (u : Set (ℕ × ℕ)) : Set (ℕ × ℕ)

Scott's operator ℓ ↦ {(n, n)} ∪ {(n, m⁺) ∣ (n, m) ∈ ℓ} on P(ℕ × ℕ).

Equations

• Domain.Neighborhood.Exercise421.leOp u = {p : ℕ × ℕ | p.1 = p.2} ∪ {p : ℕ × ℕ | ∃ (m : ℕ), (p.1, m) ∈ u ∧ p.2 = m + 1}

theorem Domain.Neighborhood.Exercise421.leOp_monotone : Monotone leOp

def Domain.Neighborhood.Exercise421.leRel : Set (ℕ × ℕ)

The relation ≤ itself, as a subset of ℕ × ℕ.

Equations

• Domain.Neighborhood.Exercise421.leRel = {p : ℕ × ℕ | p.1 ≤ p.2}

theorem Domain.Neighborhood.Exercise421.leRel_isFixed : leOp leRel = leRel

Exercise 4.21 (Scott 1981, PRG-19). ≤ solves Scott's fixed-point equation.

theorem Domain.Neighborhood.Exercise421.mem_fixedPoint_iff {u : Set (ℕ × ℕ)} (hu : leOp u = u) (n m : ℕ) : (n, m) ∈ u ↔ n ≤ m

The key step toward uniqueness: any fixed point u of leOp agrees with ≤ pointwise. By induction on the second coordinate m; the base case m = 0 uses that the successor clause cannot produce a 0 on the right.

theorem Domain.Neighborhood.Exercise421.leOp_unique {u : Set (ℕ × ℕ)} (hu : leOp u = u) : u = leRel

Exercise 4.21 (Scott 1981, PRG-19). The order relation ≤ is the unique fixed point of Scott's equation: any u with leOp u = u equals leRel.

The function [·] : ℕ → P ℕ of 4.13(3): the up-sets.

def Domain.Neighborhood.Exercise421.succImage (x : Set ℕ) : Set ℕ

Scott's x⁺ = {n⁺ ∣ n ∈ x} on P ℕ.

Equations

• Domain.Neighborhood.Exercise421.succImage x = {k : ℕ | ∃ (j : ℕ), j ∈ x ∧ k = j + 1}

def Domain.Neighborhood.Exercise421.upSet (m : ℕ) : Set ℕ

The up-set [m] = {k ∣ m ≤ k} — the value of Scott's unique function [·] of 4.13(3).

Equations

• Domain.Neighborhood.Exercise421.upSet m = {k : ℕ | m ≤ k}

theorem Domain.Neighborhood.Exercise421.upSet_zero : upSet 0 = Set.univ

[0] = ℕ: the recursion base of 4.13(3).

theorem Domain.Neighborhood.Exercise421.upSet_succ (m : ℕ) : upSet (m + 1) = succImage (upSet m)

[m⁺] = [m]⁺: the recursion step of 4.13(3).

theorem Domain.Neighborhood.Exercise421.upSet_unique (s : ℕ → Set ℕ) (h0 : s 0 = Set.univ) (hsucc : ∀ (m : ℕ), s (m + 1) = succImage (s m)) : s = upSet

Exercise 4.21 / 4.13(3) (Scott 1981, PRG-19). [·] = upSet is the unique function with [0] = ℕ and [m⁺] = [m]⁺.

The isomorphism ⟨ℕ, 0, ⁺⟩ ≅ ⟨[m], m, ⁺⟩ is addition.

def Domain.Neighborhood.Exercise421.addIso (m : ℕ) : ℕ ≃ { k : ℕ // k ∈ upSet m }

Exercise 4.21 (Scott 1981, PRG-19). The structure-preserving bijection between ⟨ℕ, 0, ⁺⟩ and ⟨[m], m, ⁺⟩ (where [m] = {k ∣ m ≤ k}, with distinguished element m and the successor ⁺). It is ordinary addition by m: n ↦ m + n.

Equations

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

theorem Domain.Neighborhood.Exercise421.addIso_apply (m n : ℕ) : ↑((addIso m) n) = m + n

The isomorphism is given by addition: addIso m n = m + n.

theorem Domain.Neighborhood.Exercise421.addIso_zero (m : ℕ) : ↑((addIso m) 0) = m

The isomorphism sends 0 to the distinguished element m of [m].

theorem Domain.Neighborhood.Exercise421.addIso_succ (m n : ℕ) : ↑((addIso m) (n + 1)) = ↑((addIso m) n) + 1

The isomorphism preserves the successor: addIso m (n⁺) = (addIso m n)⁺.

Multiplication via the hint fixed-point equation.

def Domain.Neighborhood.Exercise421.mulOp (n : ℕ) (u : Set ℕ) : Set ℕ

Scott's hint operator n·ℕ = {0} ∪ {n + m ∣ m ∈ n·ℕ} on P ℕ (for fixed n).

Equations

• Domain.Neighborhood.Exercise421.mulOp n u = {0} ∪ {k : ℕ | ∃ (m : ℕ), m ∈ u ∧ k = n + m}

theorem Domain.Neighborhood.Exercise421.mulOp_monotone (n : ℕ) : Monotone (mulOp n)

theorem Domain.Neighborhood.Exercise421.mulOp_lfp_eq_multiples (n : ℕ) : Exercise414.lfpSet (mulOp n) = {k : ℕ | ∃ (i : ℕ), k = n * i}

Exercise 4.21 (Scott 1981, PRG-19). The least solution of the multiplication equation n·ℕ = {0} ∪ {n + m ∣ m ∈ n·ℕ} is exactly the set of multiples of n.