Page 36 - Textos de Matemática Vol. 38

28 FERNANDO FERREIRA
instead of the corresponding extensional ones, and with the further axioms M1 :x✂0y↔x≤y,
M2 : x✂ρ→σ y→∀u✂ρ v(xu✂σ yv∧yu✂σ yv), and a rule RL✂
Abd∧u✂v→su✂tv∧tu✂tv , Abd → s ✂ t
where s and t are terms of Lω✂, Abd is a bounded formula and u and v are variables that do not occur free in the conclusion.
The crucial point is that we have rules instead of the axioms: ∀u✂ρ v(xu✂σ yv∧yu✂σ yv)→x✂ρ→σ y.
Note that the above formula would pose a problem for the functional interpre- tation. The rules, however, do not pose such a problem! We dubbed the new majorizability symbols ✂σ intensional because they are (partially) governed by rules. The presence of rules entails the failure of the deduction theorem in HAω✂, a feature that many do not find attractive. However, one should keep in mind that the rules are introduced for mathematical reasons and that “mathematical attraction” is partly a question of familiarity. In the end, systems where rules play an essential role must be judged by their own mathematical merits.
Even though the rules are weaker than the axioms we still have:
Lemma 4.2. The theory HAω✂ proves that the relations ✂σ are transitive and that x✂y→y✂y.Fortype1,wehavex✂1y→x≤∗1 yandx✂1xM.Moreover, Howard’s majorizability theorem also holds: For each closed term t, there is a closed term q such that HAω✂ ⊢ t ✂ q.
4.2 Bounded functional interpretation
Let us now define the bounded functional interpretation:
Definition 4.3. To each formula A of the language Lω✂ we assign formulas (A)B
,c) a bounded for- and AB so that (A)B is of the form ∃˜b∀˜cAB(b,c), with AB(b
mula, according to the following clauses:
1. (A)B and AB are simply A, for atomic formulas A.
If we have already interpretations for A and B given by ∃˜b∀˜cAB(b, c
) and ∃˜d
(respectively) then we define:
∀˜eBB(d, e
)
2 . ( A ∧ B ) B i s ∃˜ b
(AB(b,c)∧BB(d,e
, d∀˜c, e
)),