Page 22 - Textos de Matemática Vol. 38

14 FERNANDO FERREIRA
This notion reminds the notion of ∃-free formula, but notice that disjunc- tions are allowed.
Definition 2.10. To each formula A of the language Lω≤ we assign formulas (A)br
Abr(b), with Abr(b) a ∃˜-free formula, and Abr so that (A)br is of the form ∃˜b
according to the following clauses:
1. (A)br and (A)br are simply A, for atomic formulas A.
If we have already interpretations for A and B given by ∃˜b
Abr(b) and ∃˜d
(respectively) then, we define
2 . ( A ∧ B ) b r i s ∃˜ b , d
(Abr(b) ∧ Bbr(d)),
(Abr(b) ∨ Bbr(d)), 3 . ( A ∨ B ) b r i s ∃˜ b , d
Bbr (d
)
4 . ( A → B ) b r i s ∃˜ f ∀˜ b
(Abr (b
) → Bbr(f(b))). For bounded quantifiers we have:
5. (∀x ≤∗ t A(x))br is ∃˜b∀x ≤∗ t Abr(b, x),
6. (∃x ≤∗ t A(x))br is ∃˜b∃x ≤∗ t Abr(b, x). And for unbounded quantifiers we define
7. (∀xA(x))br is ∃˜f∀˜a∀x ≤∗ aAbr(f(a),x). 8. (∃xA(x))br is ∃˜a, b∃x ≤∗ a Abr(b, x).
Notice that the realizers of a disjunction do not include a flag deciding which way to go and that only a bound for the existential witness is included in the realizers of an existential statement. As usual, negation is a particular case of the implication: (¬A)br is ∀˜b¬Abr(b).
Three principles are important in connection with the above assignment: I. Bounded Choice bACω:
∀x∃yA(x, y) → ∃˜f ∀˜b∀x ≤∗ b∃y ≤∗ f b A(x, y),
where A is an arbitrary formula of the language Lω≤.
II. Bounded Independence of Premises bIPω˜ : ∃free
(A → ∃yB(y)) → ∃˜b(A → ∃y ≤∗ b B(y)),
where A is a ∃˜-free formula and B is an arbitrary formula.