Some Relations among Systems for Bounded Arithmetic

In [1], S. Buss introduced systems S 2 i (i = 0, 1, 2,…), Ů 2 1 , and $$\begin{array}{*{20}{c}} ^\circ \\ v \\ \end{array} _{2}^{1}$$ for Bounded Arithmetic which are closely related to Δ i p (if i > 0) in the polynomial hierarchy, PSPACE, and EXPTIME respectively. In Bounded Arithmetic weaker systems and stronger systems are interacted each other. As we think in physics that the basic principles are the principles on elementary particles, we believe that the intrinsic nature of Bounded Arithmetic is hidden in very weak systems of Bounded Arithmetic. Therefore it seems to us very useful to define sharply bounded arithmetic and to study it. Unfortunately S 2 0 is too weak to be a good candidate for sharply bounded arithmetic since it is proved in [7] that S 2 0 does not prove ∃x(a = 0 V x + 1 = a). On the other hand, $$\tilde S_2^0$$ introduced in [8] seems to us a good candidate for sharply bounded arithmetic. We shall prove that $$\tilde S_2^0 = \tilde S_2^1$$ implies EXPTIME = PSPACE, where $$\tilde S_2^1$$ is a conservative extension of S 2 1 , and that if $$\begin{array}{*{20}{c}} ^\circ \\ v \\ \end{array} _{2}^{1}$$ proves $$\forall {}^ \ulcorner {\varphi ^ \urcorner }\exists \operatorname{w} (\operatorname{PA} - \Pr \operatorname{f} (\operatorname{w} ,{}^ \ulcorner {\varphi ^ \urcorner })\operatorname{V} \;\operatorname{PA} - \Pr \operatorname{f} (\operatorname{w} ,{}^ \ulcorner \urcorner {\varphi ^ \urcorner }))$$ then PSPACE = NP ⋂ co-NP, where ⌜ ϕ ⌝ is a Gödel number of a sharply bounded sentence and PA — Prf(w, ⌜ ϕ ⌝) is a formalized statement “w is a proof of ⌜ ϕ ⌝ in Peano Arithmetic”.