Page 24 - Textos de Matemática Vol. 38

16 FERNANDO FERREIRA
2.4 Extraction, conservation and characterization for bounded modified realizability
Proposition 2.13. Suppose that
HAω≤ + bACω + bIPω˜ + MAJω + ∆ ⊢ ∀x∃yA(x, y),
∃free
where ∆ is a set of ∃˜-free sentences and A is a ∃˜-free formula with free variables among x and y. Then there is a closed monotone term t of appropriate type such that
H A ω≤ + ∆ ⊢ ∀˜ a ∀ x ≤ ∗ a ∃ y ≤ ∗ t a A ( x , y ) .
Strictly speaking, we do not have a conservation result. However, if the
type of x is 0 or 1 then we do have such a result: Corollary 2.14. Suppose that
HAω + bACω + bIPω + MAJω + ∆ ⊢ ∀x0/1∃yA(x, y), ≤ ∃˜free
where ∆ is a set of ∃˜-free sentences, A a ∃˜-free formula with free variables among x and y. Then there is a closed monotone term t of appropriate type such that
H A ω≤ + ∆ ⊢ ∀ x ∃ y ≤ ∗ t x A ( x , y ) .
In particular, this corollary yields a relative consistency result of the theory
HAω + bACω + bIPω + MAJω over HAω . This is clearly interesting in the ≤ ∃˜free ≤
present setting because the former theory is classically inconsistent: It refutes the classically true Markov’s principle. To see this, suppose that
∀x1¬¬∃n0(xn = 0) → ∃n0(xn = 0).
By intuitionistic logic and bIPω˜ , we may infer ∀x1∃n0(¬∀k0(xk ̸= 0) → ∃i ≤
∃free ω 0
n(xi = 0)). By the collection principle bC , there is a natural number m such
that ∀x ≤1 1(¬∀k0(xk ̸= 0) → ∃n ≤ m(xn = 0)). This is a contradiction (just consider the number-theoretic primitive recursive function that takes the value 1 for values less than m + 1 and is 0 afterwards).
Reinhard Kahle pointed to me that the above corollary can be viewed as
the success of an unconventional Hilbert’s Program for the “ideal” and rather
strange (intuitionistic) world of HAω +bACω +bIPω +MAJω. It is a world with ≤ ∃˜free
some principles related to Brouwerian intuitionism and, in the terminology of intuitionism, it has strong counterexamples to classical logic. On a more personal key, I find admirable the fact that Frege’s naive (and natural) view of sets as extensions of concepts proved to be inconsistent (Russell’s paradox) whereas the prima facia more bizarre and radical world of Brouwerian intuitionism proved to be coherent after all.1
1It is against the spirit of intuitionism to pose the question of its coherence, least of all of its formal consistency. In a sense, the coherence of intuitionistic reasoning is just the pragmatic coherence of contentual thought. Nevertheless, the question can still be posed since, after all, Frege was also a champion of language expressing contentual thought.