Abstract
Conservative subtheories of \({{R}^{1}_{2}}\) and \({{S}^{1}_{2}}\) are presented. For \({{S}^{1}_{2}}\), a slight tightening of Jeřábek’s result (Math Logic Q 52(6):613–624, 2006) that \({T^{0}_{2} \preceq_{\forall \Sigma^{b}_{1}}S^{1}_{2}}\) is presented: It is shown that \({T^{0}_{2}}\) can be axiomatised as BASIC together with induction on sharply bounded formulas of one alternation. Within this \({\forall\Sigma^{b}_{1}}\)-theory, we define a \({\forall\Sigma^{b}_{0}}\)-theory, \({T^{-1}_{2}}\), for the \({\forall\Sigma^{b}_{0}}\)-consequences of \({S^{1}_{2}}\). We show \({T^{-1}_{2}}\) is weak by showing it cannot \({\Sigma^{b}_{0}}\)-define division by 3. We then consider what would be the analogous \({\forall\hat\Sigma^{b}_{1}}\)-conservative subtheory of \({R^{1}_{2}}\) based on Pollett (Ann Pure Appl Logic 100:189–245, 1999. It is shown that this theory, \({{T}^{0,\left\{2^{(||\dot{id}||)}\right\}}_{2}}\), also cannot \({\Sigma^{b}_{0}}\)-define division by 3. On the other hand, we show that \({{S}^{0}_{2}+open_{\{||id||\}}}\)-COMP is a \({\forall\hat\Sigma^{b}_{1}}\)-conservative subtheory of \({R^{1}_{2}}\). Finally, we give a refinement of Johannsen and Pollett (Logic Colloquium’ 98, 262–279, 2000) and show that \({\hat{C}^{0}_{2}}\) is \({\forall\hat\Sigma^{b}_{1}}\)-conservative over a theory based on open cl-comprehension.
This is a preview of subscription content, log in via an institution to check access.
Similar content being viewed by others
References
Allen B.: Arithmetizing uniform NC. Ann. Pure Appl. Logic 53(1), 1–50 (1991)
Beckmann A., Buss S.R.: Polynomial local search in the polynomial hierarchy and witnessing in fragments of bounded arithmetic. J. Math. Logic 9(1), 103–138 (2009)
Beckmann, A., Buss, S.R.: Characterising definable search problems in bounded arithmetic via proof notations. In: Schindler, R. (ed.) Ways of Proof Theory, Ontos Series on Mathematical Logic, pp. 65–134 (2010)
Boughattas, S., Kołodziejczyk, L.A.: The strength of sharply bounded induction requires MSP (2009) (to appear Annals of Pure and Applied Logic)
Boughattas, S., Ressayre, J.P.: Bootstrapping I (2009) (to appear Annals of Pure and Applied Logic)
Buss S.R.: Bounded Arithmetic. Bibliopolis, Napoli (1986)
Cook, S., Nguyen, P.: Logical Foundations of Proof Complexity. Cambridge University Press (to appear in Perspectives in Logic)
Clote P.: Polynomial size Frege proofs of certain combinatorial principles. In: Clote, P., Krajíček, J. (eds) Arithmetic, Proof Theory and Computational Complexity, Oxford Science Publications, Oxford (1993)
Clote P., Takeuti G.: First-order bounded arithmetic and small boolean circuit complexity classes. In: Clote, P., Remmel, J. (eds) Feasible Mathematics II, pp. 154–218. Birkhauser, Boston (1995)
Hájek P., Pudlák P.: Metamathematics of First-Order Arithmetics. Springer, Berlin (1993)
Hanika, J.: Search problems and bounded arithmetic. Ph.D. Thesis. Charles University (2004)
Jeřábek E.: The strength of sharply bounded induction. Math. Logic Q. 52(6), 613–624 (2006)
Johannsen, J.: On sharply bounded length induction. In Proceedings of Computer Science Logic ’95, pp. 362–367. Paderborn 1995. Springer LNCS 1092. (1996)
Johannsen J.: A model-theoretic property of sharply bounded formulae, with some applications. Math. Logic Q. 44(2), 205–215 (1998)
Johannsen, J., Pollett, C.: On proofs about threshold circuits and counting hierarchies. In Proceedings of Thirteenth IEEE Symposium on Logic in Computer Science, pp. 444–452
Johannsen, J., Pollett, C.: On the \({\Delta^b_1}\)-bit-comprehension rule. In: Buss, S., Hájek, P., Pudlák, P. (eds.) Logic Colloquium ’98. ASL Lecture Notes in Logic, pp. 262–279 (2000)
Kołodziejczyk, L.A.: Phuong Nguyen and Neil Thapen. The provably total NP search problems of weak second order arithmetic. Preliminary manuscript (2009)
Krajíček J.: Bounded Arithmetic, Propositional Logic, and Complexity Theory, volume 60 of Encyclopedia of Mathematics and its Applications. Cambridge University Press, Cambridge (1995)
Krajíček J., Pudlák P., Takeuti G.: Bounded arithmetic and polynomial hierarchy. Ann. Pure Appl. Logic 52, 143–154 (1991)
Krajíček J., Skelley A., Thapen N.: NP search problems in low fragments of bounded arithmetic. J. Symb. Logic 72(2), 649–672 (2007)
Mantzivis S.-G.: Circuits in bounded arithmetic, part I. Ann. Math. Artif. Intell. 6, 127–156 (1991)
Pollett C.: Structure and definability in general bounded arithmetic theories. Ann. Pure Appl. Logic 100, 189–245 (1999)
Pollett C.: Multifunction algebras and the provability of PH ↓. Ann. Pure Appl. Logic 104, 279–303 (2000)
Pollett C.: On the bounded version of Hilbert’s tenth problem. Arch. Math. Logic 42(5), 469–488 (2003)
Pudlák P.: Fragments of bounded arithmetic and the lengths of proofs. J. Symb. Logic 73(4), 1389–1406 (2008)
Shepherdson, J.C.: Non-standard models for fragments of number theory. In Proceedings of the 1963 International Symposium at Berkeley on the Theory of Models, pp. 342–358. North-Holland, Amsterdam (1965)
Takeuti G.: RSUV isomorphisms. In: Clote, P., Krajíček, J. (eds) Arithmetic, Proof Theory and Computational Complexity, pp. 364–386. Oxford Science Publications, Oxford (1993)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Pollett, C. Conservative fragments of \({{S}^{1}_{2}}\) and \({{R}^{1}_{2}}\) . Arch. Math. Logic 50, 367–393 (2011). https://doi.org/10.1007/s00153-010-0220-9
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-010-0220-9