Page 120 - Textos de Matemática Vol. 40

108 Chapter 3. Truth Theories
Proof. Since we can replace T(x) by an equation of natural numbers, the idea of the proof is to diagonalize negated existence using dN. Let us consider the following function f := rec(λf,x.dN (λy.0)(λy.notN)(t(¬˙ (f ↓˙)))s0). So f satis- fies
0, ift(¬˙(f↓˙))=s, fx≃ notN, ift(¬˙(f↓˙))̸=s.
f is a constant function, since x does not occur on the right side of its definition. By case distinction on ¬(f 0 ↓) and f 0 ↓ we get:
¬(f0↓) → ¬(valf↓) → T(¬˙(f↓˙))
→ t(¬˙(f↓˙))=s → f0=0
→ f0↓.
f0↓ → valf↓ → T(f↓˙)
→ ¬T(¬˙(f↓˙))
→ ¬t(¬˙(f↓˙))=s.
With f 0 = dN (λy.0)(λy.sN (f x))(t(¬˙ (f ↓˙)))s0 and f 0 ↓ it follows from strict- ness that t (¬˙ (f ↓˙ )) ↓ and s ↓ hold. So we get f 0 = notN from the definition of f in contradiction to (AllN). ⊣
Since, in the general case, we have only very little functional structure on propositions, we conjecture that ∀x.P(x) is consistent with FPA, but the Proposition above shows that it cannot have a smooth recursion theoretical interpretation.
3.3 Streams in scheme
As mentioned in subsection 1.2.2, applicative theories provide a natural frame- work to study functional programming languages. Here, we will show how the concept of streams in scheme can be treated by use of our notion of pointers.10
Streams are (possibly infinite) sequences of data. Since the evaluation of scheme is strict, the subexpression of an object must be evaluated before the object itself. Therefore, obviously, the evaluation of an infinite stream then
The Section on streams is also based on [Kah99] and essentially a translation of [Kah97a, Section 2.2.7].
10The concept of streams in scheme provides total or defined initial segments of streams only, but for instance no streams containing gaps. For more extensive concepts of streams cf. e.g., [Fef96, Tal92].