Page 40 - Textos de Matemática Vol. 38

32 FERNANDO FERREIRA
It is clear that the negative translation of a bounded formula is still bounded, and it can be shown by induction on the type that the intensional majorizability relations are stable, i.e., HAω✂ ⊢ ¬¬(x ✂ y) → x ✂ y. Now, in analogy with the Dialectica interpretation, the next result is not difficult:
Theorem 4.6. Suppose that
P A ω✂ + b A C ωb d , ✂ + M A J ω✂ + ∆ ⊢ A ,
where ∆ is a set of universal sentences, PAω✂ is the classical version of HAω✂ and bACωbd,✂ is the restriction of bACω✂ to bounded matrices. Then,
H A ω✂ + b A C ωb d , ✂ + M A J ω✂ + M P ω✂ + ∆ ⊢ A g .
Remark that PAω✂ + bACωbd,✂ easily proves the intensional collection prin- ciple restricted to bounded formulas and, by classical logic, bBCCω✂ follows. The next proposition is a consequence of the combination of the negative translation with the soundness theorem:
Proposition 4.7 (Extraction and conservation). Suppose that PAω✂ + bACωbd,✂ + MAJω✂ + ∆ ⊢ ∀x∃yAbd(x, y),
where ∆ is a set of universal sentences and Abd is a bounded formula with free variables among x and y. Then there is a closed monotone term t of appropriate type such that
P A ω✂ + ∆ ⊢ ∀˜ a ∀ x ✂ a ∃ y ✂ t a A b d ( x , y ) .
For technical reasons (hinging on the fact that bounded formulas are not decidable) the verification theory is a classical theory, in contrast with the anal- ogous result of Section 3.2.
We want to use this technology in “real world” applications. The following obvious lemma is the bridge from the intensional theory to plain PAω≤:
Lemma 4.8 (Flattening). Suppose that PAω✂ + ∆ ⊢ A, where A is a sentence of the language Lω✂ and ∆ is a set of universal formulas (with bounded matrices). Then PAω≤ + ∆∗ ⊢ A∗, where B∗ is the sentence of Lω≤ obtained from B by replacing throughout the binary symbols ✂σ by the formulas ≤∗σ.
Of course, we can also “flatten” the theory PAω✂ + bACωbd,✂ into the theory PAω≤ + bACωbd. However, the latter theory is inconsistent. Let us see why. It is clear, by classical logic, that PAω✂ proves
∀x1(x≤∗1 0→x✂1 0)→∀x✂1 1(¬x✂1 0→∃n0(xn̸=0)).
If we now apply the intensional collection principle restricted to bounded for- mulas to the consequent above, then