Page 63 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 51
However, g does not have a least fixed point in the sense of ⊑(VV), for we find ¬f1 ⊑(VV) f2 ∧ ¬f2 ⊑(VV) f1. That means, f1 is not comparable with any other fixed point of g and therefore, we do not have a least fixed point.
Only for monotonic g ∈ (T → T ) we can show that lg is the least fixed point of g.
Definition 1.8.9. Let T be an arrow class as given in Definition 1.8.6. A function f∈(T →T)iscalledT monotonic,if
∀g∈T.∀h∈T.g⊑T h→fg⊑T fh.
Claims 1–5 of the following Lemma correspond to the Corollary in the appendix of Feferman [Fef92]. Furthermore, in order to show that l yields a fixed point we need the compactness property stated in the last Claim of our Lemma.
Lemma 1.8.10. Let T be the arrow class (A1 B1)∩···∩(Am Bm). We can prove in LFP that if g ∈ (T → T ) is T monotonic, then the following Claims hold for all i ≤ m.
1. ∀n.hgn∈T,
2. ∀n.hgn⊑T hg(n+1),
3. lg∈T,
4. ∀n.hgn⊑T lg,
5. lg⊑T g(lg),
6. ∀m.∃n.∀x∈Ai.x≤m→lgx⊑hgnx, 7. ∀x∈Ai.∃n.g(lg)x⊑g(hgn)x.
Proof. 1. Proof by induction on the natural numbers. For n = 0 we have hg0=b. Since∀x.¬bx↓weobviouslygethg0∈T. Assumehgn∈T. Thenwehaveg(hgn)∈T andthisyieldshg(n+1)∈T.
2. We proceed by induction on the natural numbers. As above we get ∀x.¬hg0x ↓. Hence we have ∀x ∈ Ai.hg0x ⊑ hg1x for any i. For the induction step assume h g n ⊑T h g (n + 1). Since g is T monotonic and by the previous Claim ∀n. h g n ↓ holds, we get
g(hgn)⊑T g(hg(n+1)). This yields hg(n+1)⊑T hg(n+2).
3. By Lemma 1.8.3 we find ∀x ∈ Ai.lgx↓ → ∃n.hgnx = lgx for any i. Then,byClaim1weget∀x∈Ai.lgx↓→lgx∈Bi. Hencelg∈T.