Page 21 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 13
then there is a natural number m such that
HAω0 +ACω +IPω∃free ⊢∀x≤1 1∃n≤0 mA(x,n).
The proof of this result uses Howard’s majorizability relation. Assume that ∀x ≤1 1∃n0 A(x, n) is provable in HAω0 + ACω + IPω∃free. We get,
HAω0 + ACω + IPω∃free ⊢ ∀x(x ≤1 1 → ∃n∃z
Amr (z
, x, n)).
By IPω∃free, ∀x∃n∃z(x ≤1 1 → Amr(z
soundness theorem, there is a closed term t of type 2 such that
, x, n)) is provable. As a consequence of the Amr(z, x, tx)).
HAω0 ⊢∀x(x≤11→∃z
By Howard’s majorizability result, take a closed term q such that t ≤∗2 q. It is
clear that
HAω0 + ACω + IPω∃free ⊢ ∀x ≤1 1∃n ≤0 q(11) A(x, n).
2.3 Bounded modified realizability
The new proof interpretations rely heavily on the Howard-Bezem majoriz- ability notions. In view of this fact, it is convenient to work with an extension of thelanguageLω0 (withexactlythesameterms).Firstly,weextendthelanguage Lω≤ with a primitive binary relation symbol ≤ that infixes between terms of type 0. There are now new atomic formulas, and the syntactic notions extend in the natural way. Actually, the language that we get is an extension by definitions of Lω0 because x ≤ y may be defined by a natural quantifier-free formula. In this setting, we use the primitive binary symbol to define the majorizability formu- las. Secondly, it is convenient to introduce the primitive syntactical device of bounded quantifications, i.e., quantifications of the form ∀x ≤∗ t and ∃x ≤∗ t, for terms t not containing the variable x. Bounded formulas are formulas in which every quantifier is bounded.
The theory HAω≤ is HAω0 together with the (universal) defining axiom of ≤ and the following schemes:
B∀ : ∀x≤∗ tA(x)↔∀x(x≤∗ t→A(x)),
B∃ : ∃x≤∗ tA(x)↔∃x(x≤∗ t∧A(x)).
It is clear that HAω≤ is a conservative extension of HAω0 . We say that a functional f is monotone if f ≤∗ f. In the sequel, we shall often quantify over monotone functionals. We abbreviate the quantifications ∀x(x ≤∗ x → A(x)) and ∃x(x ≤∗ x ∧ A(x)) by ∀˜xA(x) and ∃˜xA(x), respectively.
Definition 2.9. A formula of Lω≤ is called ∃˜-free if it is built from atomic formulas by means of conjunctions, disjunctions, implications, bounded quantifications and monotone universal quantifications, i.e., quantifications of the form ∀˜a.