Page 13 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 5
where γ(n) stands for the finite sequence ⟨γ(0), . . . , γ(n − 1)⟩. Therefore, the value of Φ at a point β only depends on a finite initial segment of β. In other words, Φ is determined by what happens in a countable set of finite sequences. This can be made explicit in the following way. An associate of a continuous functional Φ is an element α ∈ S1 with the following three properties:
i. If s = ⟨s0,...,sn−1⟩ is a finite sequence of natural numbers such that α(s) ̸= 0, then Φ(β) = Φ(γ) for all β,γ with β(n) = γ(n) = s. [We are identifying finite sequences s with their numerical codings – as it is done in recursion theory – when writing α(s).]
ii. In case α(s) ̸= 0, then Φ(β) = α(s) − 1 whenever s is an initial segment of β.
iii. For all β ∈ S1, there is n such that α(β(n)) ̸= 0.
Of course, we may take α satisfying the conditions above and such that:
α(s) ̸= 0 if, and only if, Φ(β) = Φ(γ) for all β,γ with β(n) = γ(n) = s. This is the so-called principal associate of Φ. For technical reasons, we do not restrict ourselves to principal associates because they need not be recursive when the functional Φ is (in the sense that type 1 inputs are considered as oracles for effecting a computation).
According to the definitions, it is clear that, for every continuous functional Φ2 with associate α, the following holds:
Φ(β) = α(β(μk(α(β(k)) ̸= 0))) − 1,
where μ is the minimization operator of recursion theory. Therefore, each con- tinuous functional of type 2 is determined by a function of type 1. By means of this type lowering procedure, we obtain a structure for Lω0 in the following manner (for simplicity, we restrict ourselves to pure types). First, for α, β ∈ S1 we define
α(β) ≃ α(β(μk(α(β(k)) ̸= 0))) − 1.
Second, we let ICF0 = N, ICF1 = S1 and, for the remaining pure cases:
ICEσ→0 ={α∈S1 :∀β∈ICFσ∃k∈N(α(β)≃k)}.
The above definition can be extended to all finite types. Let ICFω = ⟨ICFσ⟩σ∈T . Application between functionals is defined in the natural way: for α ∈ ICFσ→0 and β ∈ ICFσ , with σ ̸= 0, then AppICFω (α, β) is α(β). With a proper interpre- tation of the constants, ICFω is a model of PAω0 .
This construction can be generalized in the following way. Take U ⊆ NN closed under Turing reducibility. Define ICF0(U) = N, ICF1(U) = U and, for σ ̸= 0,1, put ICFσ(U) following the blueprint above (mutatis mutandis). Then