Page 16 - Textos de Matemática Vol. 38

8 FERNANDO FERREIRA
is majorizable. Hence, we can replace the formula ∀k(α(k) = 0) by the quantifier- free formula 2E(α) = 1 and, as a consequence, get the failure of the above form of choice with a quantifier-free matrix (although with the parameter 2E).
We finish the discussion of the majorizability functionals with two obser- vations concerning the model ECFω of the continuous functionals. First, the continuous functionals of type 2 are in M2 and, in fact, ECFω is a model of ∀x2∃y2(x ≤∗2 y). The proof of this fact uses a compactness argument. Given Φ a continuous functional of type 2, it makes sense to define the functional ΦM ∈ S2 according to the equation ΦM(α) = maxβ≤1αM Φ(β) because, for a given α ∈ S1, the set {β ∈ S1 : β ≤1 αM} is a compact subspace of the Baire space and, hence, Φ[{β ∈ S1 : β ≤1 αM}] is compact in the discrete topology of N. In other words, it is finite and we can take its maximum. By construction, Φ ≤∗2 ΦM. Addition- ally, it is not difficult to show that ΦM is continuous. Clearly, by the continuity of Φ one has
S1 = ∪s∈D{β ∈ S1 : β extends s},
where D is constituted by the finite sequences of natural numbers that determine values for Φ (i.e., such that elements of S1 that extend an element of D have the same values according to Φ). Given α ∈ S1, by compactness there is a finite Fα ⊆ D such that
{β ∈ S1 : β ≤1 αM} ⊆ ∪s∈Fα {β ∈ S1 : β extends s}.
Let n ∈ N be the maximal length of the sequences in Fα. It can now be easily argued that if α(n) is an initial segment of γ then ΦM(γ) = ΦM(α).
The second observation is that, nevertheless, ECFω does not satisfy the majorizability axioms. It is well known that there is a Fan functional F3 in ECFω such that
∀Φ2∀α ≤1 1∀β ≤1 1 (α(F(Φ)) = β(F(Φ)) → Φα = Φβ).
In other words, F(Φ) is a length witnessing the uniform continuity of Φ restricted to the Cantor space (i.e., to the compact subset of the Baire space constituted by the elements α such that α ≤1 11). However, the set {F(Φ) : Φ ≤∗2 12} is clearly unbounded. Therefore, F is not majorizable in ECFω. (I thank Dag Normann for this observation.)
6. The term model. We say that a term t contracts to a term q if one of the following clauses is satisfied:
(i) tisΠrsandqisr,
(ii) t is Σrst and q is r(t, st),
(iii) t is R0st and q is s,
(iv) t is R(Sr)st and q is t(Rrst,r).