Page 14 - Textos de Matemática Vol. 38

6 FERNANDO FERREIRA
ICFω(U) := ⟨ICFσ(U)⟩σ∈T is a model of PAω0 . A particularly nice source of (counter-)examples is ICFω(Rec), where Rec is the set of (total) recursive func- tions from N to N. This is due to the fact that recursive sets do not necessarily separate disjoint r.e. sets (a result of Kleene).
4. The extensional counterparts HEOω and ECFω. The models HROω and ICFω are called intensional because the scheme of extensionality fails to hold for them. For instance, take e1,e2 ∈ N two different indices for the constant zero function. Clearly, e1,e2 ∈ HRO1. Let e ∈ N be an index for the iden- tity function. Of course, e ∈ HRO2. Even though {e}(e1) ̸= {e}(e2), one has ∀n ∈ HRO0 ({e1}(n) = {e2}(n)). Therefore, the form of extensionality
∀Φ2∀α1, β1(∀k0(αk = βk) → Φα = Φβ),
already fails in HROω. The above form of extensionality holds in ICFω, but it
is easy to find a counter-example a type higher, i.e. to: ∀G3∀Φ2, Ψ2(∀α1(Φα = Ψα) → GΦ = GΦ).
We now define the extensional counterparts of HROω and ICFω. These are called, respectively, the hereditarily effective operations HEOω and the (exten- sional) continuous functionals ECFω. The elements of non-zero type of HEOω and ECFω are functions (functionals). For HEOω we define by induction on the type σ both the functionals in HEOσ and the indices of these functionals (these indices are natural numbers). We let HEO0 be the set of natural numbers and declare that each natural number is an index of itself. We say that a natural number e is an index for a function (functional) F : HEOσ → HEOτ if for each index x of a function h of HEOσ, {e}(x) is defined and is an index for the function F(h). We take HEOσ→τ as the set of functions F : HEOσ → HEOτ which have an index. The structure HEOω is defined as ⟨HEOσ⟩σ∈T .
Regarding ECFω, we let ECF0 be the set of natural numbers and, for each non-zero type σ, we define by induction both the functionals in ECFσ and the associates of these functionals (these are elements of S1). We put ECF1 as S1 and declare each α ∈ S1 an associate of itself. We restrict to pure types in order to simplify. We say that α ∈ S1 is an associate for a function F : ECFσ → N, with σ a non-zero pure type, if for each associate β of a function h of ECFσ, α(β) is defined and is the natural number F(h). We take ECFσ→0 as the set of functions F : ECFσ → N which have an associate. This definition can be extended to all finite types. The structure ECFω is defined as ⟨ECFσ⟩σ∈T .
The structure ECFω is also called the structure of the countable functionals (Kleene’s terminology). In a way similar to the intensional case, we can also start with any subset U of S1 closed under Turing reducibility, and get the structure ECFω(U). It is a non-trivial result that ECFω(Rec) is isomorphic to HEOω (this is a wide generalization of an old result of George Kreisel, Daniel Lacombe and Joseph Shoenfield).