Page 64 - Textos de Matemática Vol. 40

52
Chapter 1. Applicative theories
4. Wehavetoshow∀x∈Ai.hgnx⊑lgxforalli. Soassumex∈Ai and h g n x ↓. We conclude l g x ↓ by Lemma 1.8.3. Hence there exists a natural number m with
hgmx = lgx. (11) From Claim 2 we get by induction
∀n,m.∀x ∈ Ai.hgnx ↓∧hgmx ↓ → hgnx = hgmx. Byx∈Ai and(11)wethereforefinallyobtainhgnx⊑lgx.
5. We have to show ∀x ∈ Ai.lgx⊑g(lg)x for all i. So let x ∈ Ai and lgx ↓. Then by Lemma 1.8.3 we get ∃n.lgx = hgnx. By the definition of h we see∀x.¬hg0x↓. Hence∃n.lgx=hg(n+1)x. Thisis
∃n.lgx = g(hgn)x. (12)
For this natural number n we have by Claim 4 that h g n ⊑T l g. Because g is T monotonic we obtain g(hgn)⊑T g(lg) and since x ∈ Ai this implies g(hgn)x⊑g(lg)x. Finally,weconcludeby(12)thatlgx⊑g(lg)x.
6. Proof by induction on m. For m = 0 the Claim follows from Lemma 1.8.3. For the induction step assume
∃n1.∀x ∈ Ai.x ≤ m → l g x ⊑ h g n1 x. Employing Lemma 1.8.3 we find
m+1∈Ai ∧lg(m+1)↓→∃n2.lg(m+1)=hgn2(m+1). Taken together this yields
∃n1, ∃n2.∀x ∈ Ai.x ≤ m + 1 ∧ l g x ↓ → l g x = h g n1 x ∨ l g x = h g n2 x. By Claim 2 and Lemma 1.8.7 we get
∃n1,n2.∀x∈Ai.x≤m+1∧lgx↓→lgx=hg(n1 +n2)x. We finally conclude
∃n.∀x ∈ Ai.x ≤ m + 1 → l g x ⊑ h g n x.
7. Proof by contrapositive: suppose there exists an x ∈ Ai so that
∀n.¬(g (l g) x ⊑ g (h g n) x). (13)
Withthisx∈Ai wedefineatermkby
k := λf.ds 0notN (g(a(lg)f)x)(g(lg)x).