Page 60 - Textos de Matemática Vol. 40

48 Chapter 1. Applicative theories
Proof. The first Claim is a consequence of the Theorem about λ abstraction. For the second Claim we have:
p1 (p0 (μrec (λy.c3 (q, g, x, p0 y, p1 y)))) ↓
lgx↓ ↔
↔ μrec(λy.c3(q,g,x,p0y,p1y))↓
↔ ∃n.c3 (q,g,x,p0 n,p1 n) = 0
↔ ∃n.qgxn↓
↔ ∃n.ds 0notN (hg(p0 n)x)(p1 n) ↓
↔ ∃n.hgnx↓.
The third Claim follows by:
p1(p0(μrec(λy.c3(q,g,x,p0y,p1y))))=z
lgx=z →
→ ∃n.p1(p0n)=z∧μrec(λy.c3(q,g,x,p0y,p1y))=n
→ ∃n.p1(p0n)=z∧c3(q,g,x,p0n,p1n)=0
→ ∃n.p1(p0n)=z∧qgx(p0n)↓
→ ∃n.p1(p0n)=z∧ds0notN(hg(p0(p0n))x)(p1(p0n))↓
→ ∃n.p1(p0n)=z∧hg(p0(p0n))x=p1(p0n)
→ ∃n.hg(p0(p0n))x=z
→ ∃n.hgnx=z. ⊣
We define the closed term a which will later serve to show that the term g (l g) can be replaced by a “finite approximation” g (h g n), cf. Lemma 1.8.10, Claim 7.
Definition 1.8.4. Let t be such that
c(λx.xx,f,x)
t f (pN x) ∗ c (λx.x x, f, x)
tfx≃
We define the term a using λ abstraction so that

agfx≃
notN g x
Lemma 1.8.5. LFP proves:
1. ∀g,f.¬ff ↓→∀n.agfn≃gn,
2. ∀g,f.ff ↓→∃m.∀n.agfn↓→agfn=gn∧n<m.
Proof. ¿From the axioms about computability we obtain by induction: ∀f, n.t f n = 0 ∨ t f n = 1
if x = 0, otherwise.
if t f x = 0, otherwise.