Page 25 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 17
Question 1. Find a semantics for the theory HAω + bACω + bIPω + MAJω . ≤ ∃˜free
Question 2. Can we consistently add full-extensionality to the theory HAω≤ + bACω +bIPω˜ +MAJω?
∃free
We can also prove a characterization theorem for bounded modified real-
izability:
Theorem 2.15 (Characterization). For any formula A,
HAω≤ +bACω +bIPω˜ +MAJω ⊢A↔(A)br. ∃free
If we prove ∀x1∃yA(x, y) in the extended theory HAω≤ + bACω + bIPω˜ + ω ∃free
MAJ for an arbitrary A then, in complete analogy with the traditional case, we
can find a closed monotone term t such that ∀x1∃y ≤∗ txA(x,y) is provable in
HAω≤ +bACω +bIPω˜ +MAJω . However, the extended theory is not a true theory
∃free 1 ∗ and, therefore, we may not conclude that the statement ∀x ∃y ≤
tx A(x, y) is true. In other words, the extraction of the term t is not sound when the matrix A is arbitrary. However, as we saw above, the extraction is indeed sound if A(x, y)
is an ∃˜-free formula (in particular, if A(x, y) is quantifier-free). 2.5 Benign principles
In the context of bounded modified realizability, if we are interested in
extracting sound bounding information from (formalizable) proofs, we must
restrict ourselves to conclusions of the form ∀∃ whose matrix is ∃˜-free. If such
statements are proved in the theory HAω≤ + bACω + bIPω˜ + MAJω , then it is ∃free
possible to extract truthful bounding information. Of course, we may use in our proofs principles that follow from the above theory. This is the case, e.g., with Kohlenbach’s uniform boundedness principles UBρ, a combination of the Fan theorem (extended to higher types) with choice:
∀k0∀x ≤ yk∃z0A(x,y,k,z) → ∃χ1∀k0∀x ≤ yk∃z ≤ χkA(x,y,k,z),
for arbitrary A and y of type 0 → ρ.
There are, however, principles that do not follow from the extended theory
but whose use as premises do yield truthful bounding information. This is so with principles whose bounded realization can be checked in a true theory. We call these principles benign (simultaneously benign, in fact). Note that benign principles may be false. We present a list of nine benign principles:
1. The axioms of extensionality ∀zσ→δ∀xσ,yσ(x =σ y → zx =δ zy), for σ = 0, 1 or 2 and δ arbitrary, are benign.
2. The classical, but not intuitionistic, truth ∀x∀y(A(x) ∨ B(y)) → ∀xA(x) ∨ ∀yB(y),