Page 23 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 15
III. Majorizability Axioms MAJω: ∀x∃y(x ≤∗ y).
Actually, this principle is a consequence of bIPω˜ . To see this, take any xσ ∃free
and remark that the implication ∃zσ(z =σ x) → ∃˜y∃z ≤∗σ y(z =σ x) is a consequence of bIPω˜ by putting A as 0 = 0. It follows ∃˜y∃z ≤∗σ y(z =σ x).
∃free ∗ ∗ ω Now, the implication z =σ x∧z ≤σ y → x ≤σ y is provable in HA0 (no
extensionality is needed here). The majorizability axiom follows.
It must be remarked that each principle above is false in the full set the-
oretical model Sω. The majorizability axioms MAJω (as well as bIPω˜ ) are, of ω ∃free
course, true in the structure M of the majorizable functionals. However, as we saw in the first lesson, the bounded choice principle already fails in Mω for x of type 1 and y of type 0.
Proposition 2.11. The theory HAω≤ + bACω + bIPω˜ proves the Collection Prin- ciple bCω: ∃free
∀z ≤∗ c∃yA(y, z) → ∃˜b∀z ≤∗ c∃y ≤∗ bA(y, z),
where A is an arbitrary formula and c is monotone.
Proof. Suppose that ∀z ≤∗ c∃yA(y, z). By bIPω˜ , we get ∃free
∀z∃˜b(z ≤∗ c → ∃y ≤∗ bA(y, z)).
By bACω , we may conclude that ∃˜f ∀z ≤∗ c∃˜b ≤∗ f c∃y ≤∗ b A(x, y). The desired
conclusion follows from the transitivity of the majorizability relation.
The case where the types of z and y are 0 extends the familiar collection principle of arithmetic. In the context of intuitionistic analysis, Brouwer’s Fan theorem is the case where z is of type 1 and y is of type 0. The formulation for the Cantor space is:
∀z ≤1 1∃n0A(n, z) → ∃m0∀z ≤1 1∃n ≤ mA(n, z),
for arbitrary formulas A. The above formulation of the Fan theorem must be distinguished from the following, which also appears in the literature:
w(k) = z(k) → A(n, w)), ∀z ≤1 1∃n0A(n, z) → ∃k0∀z ≤1 1∃n0∀w ≤1 1(
for arbitrary formulas A. The latter formulation explicitly includes a continuity principle, whereas the former does not. It is important to keep in mind that bounded interpretations concern majorizability notions, not continuity notions.
Theorem 2.12 (Soundness of bounded modified realizability). Suppose that HAω≤ +bACω +bIPω˜ +MAJω +∆⊢A(z),
∃free
where ∆ is a set of ∃˜-sentences and A(z) is an arbitrary formula (with the free variables as shown). Then there are closed monotone terms t of appropriate types such that
H A ω≤ + ∆ ⊢ ∀˜ a ∀ z ≤ ∗ a A b r ( t a , z
).