Page 37 - Textos de Matemática Vol. 38

PROOF INTERPRETATIONS 29
3 . ( A ∨ B ) B i s ∃˜ b
4 . ( A → B ) B i s ∃˜ f , g ∀˜ b
For bounded quantifiers we have:
5. (∀x ✂ tA(x))B is ∃˜b∀˜c∀x ✂ t AB(b, c, x),
6. (∃x ✂ tA(x))B is ∃˜b∀˜c∃x ✂ t∀˜c′ ✂ c AB(b
, c′, x).
And for unbounded quantifiers we define:
7. (∀xA(x))B is ∃˜f∀˜a,c
∀˜c
, d∀˜c, e
(∀˜c′ ✂ cAB(b, c′) ∨ ∀˜e′ ✂ eBB(d, e′)),
,e(∀˜c✂gbeAB(b
,c) → BB(fb,e
)).
∀x✂aAB(fa,c,x),
∃x ✂ a∀˜c′ ✂ cAB(b, c′, x).
There are five important principles in connection with this interpretation:
8 . ( ∃ x A ( x ) ) B i s ∃˜ a , b
I. Intensional Bounded Choice bACω✂:
∀ x ∃ y A ( x , y ) → ∃˜ f ∀˜ b ∀ x ✂ b ∃ y ✂ f b A ( x , y ) ,
where A is an arbitrary formula of Lω. Clearly, the forms of choice bACi,j,
✂ qf ∀xi∃yjAqf(x,y) → ∃f∀x∃y ≤j fxAqf(x,y), for i,j ∈ {0,1}, follow from bACω✂ in HAω✂ (even if bACω✂ were restricted to bounded matrices only). Due to bounded
minimization, note that bACi,0 ⇒ ACi,0 , for i ∈ {0, 1}. qf qf
II. Intensional Bounded Independence of Premises bIPω✂: ( A → ∃ y B ( y ) ) → ∃˜ b ( A → ∃ y ✂ b B ( y ) ) ,
where A is a universal formula (with bounded matrix) and B is an arbitrary formula.
III. Intensional Bounded Markov’s Principle MPω✂: (∀yAbd(y) → Bbd) → ∃˜b(∀y ✂ bAbd(y) → Bbd),
where Abd is a bounded matrix and Bbd is a bounded formula. When B is the formula 0 = 1, the above principle specializes to ¬∀yAbd(y) → ∃˜b¬∀y✂bAbd(y). If y is of type 0 and the matrix is quantifier-free, the principle further specializes to the familiar Markov’s principle of type 0: ¬∀yAqf (y) → ∃y¬Aqf (y). In this, we are using bounded numerical search.
IV. Intensional Bounded Contra-Collection Principle bBCCω✂: ∀˜b∃z ✂ c∀y ✂ bAbd(y, z) → ∃z ✂ c∀yAbd(y, z),