Page 12 - Textos de Matemática Vol. 38

4 FERNANDO FERREIRA
Using the recursors, it is possible to associate to each description of a primitive recursive function a closed term that (with the proper understanding) satisfies the defining conditions of the description. Therefore, the theory HAω0 contains, in a natural sense, primitive recursive arithmetic. Actually, only the recursor R0 is needed to define the primitive recursive functions. The presence of recursors of higher types has the effect of making possible the definition of functions beyond the primitive recursive functions (e.g., the Ackermann func- tion).
We reserve the subscript “qf” for quantifier-free formulas:
Proposition 1.2. For each quantifier-free formula Aqf(x) there is a closed term
tofappropriatetypesuchthatHAω0 ⊢Aqf(x)↔tx=0.
As a consequence, HAω0 ⊢ Aqf ∨ ¬Aqf . The theory obtained from HAω0 by adjoining the unrestricted law of excluded middle A ∨ ¬A is the classical theory PAω0 . If full extensionality is present, we have E-PAω.
1.4 Main models
1. The full set-theoretical model Sω . Let S0 = N and Sρ→τ = (Sτ )Sρ , where (Sτ)Sρ is the set of all functions from Sρ to Sτ. Let Sω be ⟨Sσ⟩σ∈T . With the proper understanding, it is clear that Sω is a model of HAω0 . It is actually a model of E-PAω. The model Sω is called the standard structure of finite type arithmetic. When we call a sentence of Lω0 true or false, we always mean true or false with respect to the standard model.
2. The hereditarily recursive operations HROω. For each type σ we define a subset HROσ of the natural numbers in the following way: HRO0 = N and
HROρ→τ ={n∈N:∀k∈HROρ∃m∈HROτ ({n}(k)≃m)},
where {·} denotes the Kleene bracket of recursion theory. Let HROω be ⟨HROσ ⟩σ∈T . If n ∈ HROρ→τ and k ∈ HROρ then AppHROω (n, k) is defined as {n}(k). With a proper interpretation of the constants, HROω is a model of PAω0 . By internalizing the above definitions within first-order Heyting arithmetic HA, it is possible to prove the following conservation result:
Proposition 1.3. The theory HAω0 is conservative over HA.
3. The intensional continuous functionals ICFω. In order to motivate some def- initions below let us briefly discuss continuous functionals of type 2. The set S1 endowed with the product topology of the discrete space N with itself N-times is known as the Baire space. It is easy to see that a functional Φ : S1 → N is continuous at a point β ∈ S1 if, and only if,
∃n ∈ N∀γ ∈ S1(
γ(n) = β(n) → Φ(γ) = Φ(β)).