Page 35 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 27
3. Peano’s theorem on the local existence theorem for solutions of (finite systems of) ordinary differential equations.
4. G¨odel’s completeness theorem: every countable consistent set of sentences in first-order logic has a countable model.
5. Every countable commutative ring has a prime ideal.
6. Brouwer’s fixed point theorem: every uniformly continuous function φ :
[0, 1]n → [0, 1]n has a fixed point.
7. The separable Hahn-Banach theorem: if f is a bounded linear functional
on a subspace of a separable Banach space, and if ||f|| ≤ 1, then f has a ˜˜
linear extension f to the whole space such that ||f|| ≤ 1.
We shall show in the next lesson that the provably total Σ01-functions of WKL0 are still the primitive recursive functions, a result originally due to Harvey Friedman.
4 Fourth lecture
4.1 Intensional majorizability
Bounded formulas are treated as computationally empty by the bounded modified realizability interpretation, in the sense that their realizers are trivial. This hinges on the fact that the majorizability relations of Howard-Bezem are given by ∃˜-free formulas and that these formulas have trivial realizers. However, the functional interpretation acts non-trivially on these formulas. We solve this problem with the notion of intensional majorizability.
We introduce a modification of the language Lω≤, dubbed Lω✂. The new language is an extension of Lω0 with the primitive binary relation symbol ≤ (as in Lω≤), but also with primitive binary relation symbols ✂σ, for each type σ. Note that the terms of Lω✂ and Lω0 are the same. The symbols ✂σ are the intensional counterparts of ≤∗σ. There are now new atomic formulas, and the syntactic device of bounded quantification is modified in such a way that it now concerns the intensional symbols instead of the extensional ones. I.e., we have quantifications of the form ∀x✂tA(x) and ∃x✂tA(x), for terms t not containing x. In the current framework, we use the terminology of the bounded formulas and monotone functionals with respect to the intensional symbols.
Definition 4.1. The theory HAω✂ is an altered version of HAω≤ with the axiom schemes:
B∀ : ∀x✂tA(x)↔∀x(x✂t→A(x)), B∃ : ∃x✂tA(x)↔∃x(x✂t∧A(x)),