Page 65 - Textos de Matemática Vol. 40

1.8. A case study: least fixed points 53
For the so defined k we will show that either assumption ¬kk ↓ or kk ↓ leads to a contradiction. As a consequence we conclude that there cannot exist an x ∈ Ai satisfying (13) and hence this Claim is proven.
Now suppose ¬ k k ↓. As a direct consequence of Lemma 1.8.5 we obtain for any j
Therefore, we get
∀f.¬ff ↓→∀y∈Aj.a(lg)fy≃lgy. ∀y ∈ Aj .a (l g) k y ≃ l g y
for any j. The term a is defined by λ abstraction. Hence by Theorem 1.2.1 and Claim 3 we find a(lg)k ∈ T. Therefore we obtain by the T monotonicity of g and x ∈ Ai that g(a(lg)k)x ≃ g(lg)x. By (13) it is the case that g(lg)x ↓. Hence g(a(lg)k)x = g(lg)x. This implies
ds 0notN (g(a(lg)k)x)(g(lg)x) ↓,
i.e., (λf.ds 0notN (g(a(lg)f)x)(g(lg)x))k ↓ and kk ↓. Contradiction.
Suppose kk ↓. Hence ds 0notN (g(a(lg)k)x)(g(lg)x) ↓ and
g(a(lg)k)x = g(lg)x. (14)
By Lemma 1.8.5 k k ↓ implies for any j
∃m.∀y ∈ Aj . a (l g) k y ↓ → a (l g) k y = l g y ∧ y < m. (15)
Using Claim 6 we get ∃n.∀y ∈ Aj.a(lg)ky ⊑ hgny. for any j. Hence ∃n.a(lg)k⊑T hgn. Claim3togetherwith(15)yieldsa(lg)k∈T. Since g is T monotonic we therefore have
∃n.g(a(lg)k)⊑T g(hgn). Our assumption x ∈ Ai yields
∃n.g (a (l g) k) x ⊑ g (h g n) x. (16) From (13) we know ∀n.¬(g (l g) x ⊑ g (h g n) x). Using (16) we conclude
¬(g(lg)x = g(a(lg)k)x)
The following Theorem states that l indeed yields a fixed point of a mono-
which contradicts (14). tonic operation g.
⊣
Theorem 1.8.11. We can prove in LFP that if g ∈ (T → T ) is T monotonic for T given as in Definition 1.8.6, then
lg∼=T g(lg).