Exercise 4.13 (Scott 1981, PRG-19, Lecture IV) — eliminating the circularity

The proof of Theorem 4.1 uses the integers (the chain fⁿ(⊥)), whereas the proof of Theorem 4.6 uses 4.1 — a hint of circularity. Scott shows it can be eliminated:

(1) If a domain 𝒟 has an element a where, for f : 𝒟 → 𝒟, the relation f(a) ⊑ a holds, then the least fixed point can be defined without the integers, purely by a greatest-lower-bound:

fix(f) = ⋂ {x ∈ |𝒟| ∣ f(x) ⊑ x},

and fix(f) ⊑ a. Here b = ⋂{…} is a well-defined element by Exercise 1.18 (sInf, the intersection of a non-empty family of filters). The argument uses only the monotonicity of f : |𝒟| → |𝒟| — no directed sups, no integers:

• f(b) ⊑ x whenever f(x) ⊑ x (since b ⊑ x so f(b) ⊑ f(x) ⊑ x), hence f(b) ⊑ b;
• then f(f(b)) ⊑ f(b), so b ⊑ f(b) too; thus b = f(b);
• b is least among pre-fixed points, in particular the least fixed point.

This is monoFix / monoFix_isFixed / monoFix_least / monoFix_le_preFix below. It is entirely choice-free (#print axioms ⊆ {propext, Quot.sound}).

(2) The argument uses only monotonicity, and (1) always applies to power-set domains P A (take a = A, the top element, where f(A) ⊑ A is automatic) — see Exercise 4.14.

(3) With (1) one re-establishes the recursion principle behind 4.6 directly: for any structured set ⟨Z, z, ·⟩ there is a unique s : ℕ → Z with s(0) = z and s(n⁺) = s(n)· (exists_unique_nat_rec). This is the choice-free primitive recursion theorem; combined with (1) it removes the circularity (one no longer needs 4.1 to build the iteration).

(4) Specializing (3) to ⟨ℕ, 0, ⁺⟩ recovers the very iteration n ↦ fⁿ used in 4.1 (nat_iterate_unique), closing the loop without circularity.

(1) The least fixed point of a monotone map via intersection.

def Domain.Neighborhood.NeighborhoodSystem.preFix {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) : Set V.Element

The set of pre-fixed points {x ∣ f(x) ⊑ x} of f.

Equations

• Domain.Neighborhood.NeighborhoodSystem.preFix f = {x : V.Element | f x ≤ x}

@[simp]

theorem Domain.Neighborhood.NeighborhoodSystem.mem_preFix {α : Type u_1} {V : NeighborhoodSystem α} {f : V.Element → V.Element} {x : V.Element} : x ∈ preFix f ↔ f x ≤ x

def Domain.Neighborhood.NeighborhoodSystem.monoFix {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) {a : V.Element} (ha : f a ≤ a) : V.Element

Exercise 4.13(1) (Scott 1981, PRG-19). The least fixed point of a monotone f defined purely as the greatest lower bound of the pre-fixed points, ⋂ {x ∣ f(x) ⊑ x}. Well-defined as an element by Exercise 1.18 (sInf); the non-emptiness witness is any a with f(a) ⊑ a.

Equations

• Domain.Neighborhood.NeighborhoodSystem.monoFix f ha = V.sInf (Domain.Neighborhood.NeighborhoodSystem.preFix f) ⋯

theorem Domain.Neighborhood.NeighborhoodSystem.monoFix_le_preFix {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) {a : V.Element} (ha : f a ≤ a) {x : V.Element} (hx : f x ≤ x) : monoFix f ha ≤ x

monoFix f ha ⊑ x for every pre-fixed point x (f(x) ⊑ x).

theorem Domain.Neighborhood.NeighborhoodSystem.monoFix_le {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) {a : V.Element} (ha : f a ≤ a) : monoFix f ha ≤ a

monoFix f ha ⊑ a: the least fixed point lies below the given pre-fixed point a.

theorem Domain.Neighborhood.NeighborhoodSystem.monoFix_preFix {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) {a : V.Element} (ha : f a ≤ a) : f (monoFix f ha) ≤ monoFix f ha

The key step: f(b) ⊑ b where b = monoFix f ha, by monotonicity alone.

theorem Domain.Neighborhood.NeighborhoodSystem.monoFix_isFixed {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) (hf : Monotone f) {a : V.Element} (ha : f a ≤ a) : f (monoFix f ha) = monoFix f ha

Exercise 4.13(1) (Scott 1981, PRG-19). monoFix f ha is a fixed point: f(b) = b. (After f(b) ⊑ b, monotonicity gives f(f(b)) ⊑ f(b), so f(b) is itself a pre-fixed point, whence b ⊑ f(b).)

theorem Domain.Neighborhood.NeighborhoodSystem.monoFix_least {α : Type u_1} {V : NeighborhoodSystem α} (f : V.Element → V.Element) {a : V.Element} (ha : f a ≤ a) {y : V.Element} (hy : f y = y) : monoFix f ha ≤ y

Exercise 4.13(1) (Scott 1981, PRG-19). monoFix f ha is the least fixed point: any y with f(y) = y satisfies b ⊑ y.

(3) The primitive-recursion theorem (choice-free), behind 4.6.

theorem Domain.Neighborhood.NeighborhoodSystem.exists_unique_nat_rec {Z : Type u_2} (z : Z) (op : Z → Z) : ∃! s : ℕ → Z, s 0 = z ∧ ∀ (n : ℕ), s (n + 1) = op (s n)

Exercise 4.13(3) (Scott 1981, PRG-19). For any structured set ⟨Z, z, ·⟩ (z : Z, op : Z → Z) there is a unique s : ℕ → Z with s(0) = z and s(n⁺) = (s n)·. This is the choice-free recursion principle (Nat.rec); together with 4.13(1) it eliminates the circularity in the proofs of 4.1 and 4.6.

(4) Specialization to ⟨ℕ, 0, ⁺⟩.

theorem Domain.Neighborhood.NeighborhoodSystem.nat_iterate_unique {s : ℕ → ℕ} (h0 : s 0 = 0) (hsucc : ∀ (n : ℕ), s (n + 1) = s n + 1) (n : ℕ) : s n = n

Exercise 4.13(4) (Scott 1981, PRG-19). Specializing 4.13(3) to the structured set ⟨ℕ, 0, ⁺⟩: the unique function s with s(0) = 0 and s(n⁺) = (s n)⁺ is the identity. This is the iteration n ↦ fⁿ underlying Theorem 4.1, now justified without circularity.