Page 15 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 7
5. The majorizable functionals Mω. Fix a suitable formula x ≤ y saying that the natural number x is less than or equal to the natural number y. The ma- jorizability formulas ≤∗σ of Howard-Bezem are defined inductively on the types according to the following clauses:
(a) x≤∗0 y:=x≤y,
(b) x≤∗ρσ y:=∀uρ,vρ(u≤∗ρ vxu≤∗σ yv∧yu≤∗σ yv).
For x, y ∈ S1, x ≤∗1 y iff x is pointwise below y and y is non-decreasing. It follows that ≤∗1 is not reflexive.
Lemma 1.4. For each type σ, HAω0 proves that ≤∗σ is transitive and x ≤∗σ y → y ≤ ∗σ y .
Mρ Mρ∗r
LetM0 =NandMρ→τ ={x∈Mτ :∃y∈Mτ (x≤ρ→τ y)},where
the superscript r means that the quantifiers of the formula x ≤∗ρ→τ y relativize to the Mτ ’s. Let Mω be ⟨Mσ ⟩σ∈T . Even though there are functionals which are not majorizable, William Howard showed the following:
Theorem 1.5. For each closed term t there is a closed term q such that HAω0 ⊢ t ≤∗ q.
An adaptation of the above result shows that Mω is a model of E-PAω. By construction, it is even a model of the majorizability axioms MAJω: ∀x∃y(x≤∗ y). Given α : N → N, let αM be defined by αM(n) = maxk≤n α(k). It is clear that α ≤∗1 αM. Therefore, M1 = S1. However, M2 is properly contained in S2. In other words, Sω is not a model of MAJω (the majorizability axioms fail already
at type 2). E.g., consider the functional Σ ∈ S2 defined as follows: Σ(α)= n ifnistheleastvaluesuchthatα(n)̸=0,
0 if ∀k (α(k) = 0).
Suppose, in order to get a contradiction, that there is Ψ with Σ ≤∗2 Ψ. In particular, ∀α ∈ S1(α ≤∗1 11 → Σ(α) ≤ Ψ(11)). This is a contradiction: just consider the function α which takes the value 0 for numbers n ≤ Ψ(11) and is 1 afterwards. As a consequence, the following form of choice fails in Mω: ∀α1∃n0A(α, n) → ∃Φ2∀α1 A(α, Φ(α)). To see this, just take for A the formula:
(α(n) ̸= 0 ∧ ∀k < n(α(k) = 0)) ∨ (n = 0 ∧ ∀k(α(k) = 0)).
The failure of choice in Mω can be further improved by noticing that the dis-
continuous functional 2E defined thus:
2E(α) = 1 if ∀k(α(k) = 0) 0 otherwise