Page 61 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 49
and
∀f, n, m.m ≤ n ∧ t f m = 0 → t f n = 0.
Now, we get the first Claim by:
¬ff↓ →
→ ∀n.c (λx.x x, f, n) = 1
→ ∀n.tfn=1
→ ∀n.ds notN (gn)(tf n)0 ≃ gn
→ ∀n.agf n ≃ gn.
The second Claim follows with:
(λx.xx)f↓
¬(λx.xx)f↓
ff↓ →
→ ∃m.c(λx.xx,f,m)=0
→ ∃m.tfm=0
→ ∃m.∀n.m≤n→tfn=0
→ ∃m.∀n.tfn̸=0→n<m
→ ∃m.∀n.agfn↓→agfn=gn∧n<m. ⊣
Since there is not a least fixed point for every recursion equation, cf. Ex- ample 1.8.8 below, we can only expect a meaningful solution for functionals satisfying an additional property, namely monotonicity. To define this notion, we will first introduce the concept of classes.
An Ll formula A containing exactly x as free variable will be called a class.8 Let A and B be classes and let φ be an arbitrary formula of Ll. We will employ the following abbreviations:
t∈A := t↓∧A[t/x],
A→B := ∀y.y∈A→xy∈B,
AB := ∀y.y∈A∧xy↓→xy∈B, A∩B := x∈A∧x∈B,
∀x∈A.φ(x) := ∀x.x∈A→φ(x).
Notethatt∈Ahasastrictnesspropertybuiltin. Wehavet∈A→t↓. Next we are going to introduce the definedness ordering ⊑T with respect to a class T. The meaning of r ⊑ s is, that if r has a value, then r equals s; and f ⊑AB g says, that for every x ∈ A, if the computation f x terminates, then g x also terminates and both computations yield the same result.
8This notion is somehow ad hoc. We will introduce later another notion of class for truth theories which should not be confused with the one used here. Tactically we use here the letters A and B for formulae (instead of φ and ψ), just in the cases where they should represent classes.