Abstract
We characterize the bounded first order consequences of theory in U 12 terms of a limited use of exponentiation, we construct a simulation of U 12 by the quantified propositional calculus, and we prove that U 12 is not conservative over IΔ0 and that it is stronger than a conservative Δ 1,b1 -extension of S 2. As corollaries we obtain that U 12 is not conservative over TNC and that ∑ bj -consequences of U 21 are finitely axiomatizable (j ≥ 2). We also show that Ů 12 plus a version of ∏ 1,b1 -SEP is conservative over U 12 (BD) w.r.t. bounded formulas.
On leave from the Mathematical Institute on Prague.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
S. Buss, “Bounded Arithmetic,” Bibliopolis, Napoli, 1986.
S. Buss, Axiomatizations and Conservation Results for Fragments of Bounded Arithmetic, to appear Contemporary Mathematics AMS, Proc. of Workshop in Logic and Computation, (1987).
P. Clote-G. Takeuti, Bounded Arithmetic for NC, Alog TIME, L and NL typescript.
S. Cook, Feasibly Constructive Proofs and the Propositional Calculus, Proc. 7th Annual ACM Symp. Th. of Comp..
M. Dowd, Propositional Representation of Arithmetic Proofs, 10th STOC (1978), 246–252, San Diego.
J. Hastad, “Comp utational Limitations of Small-Depth Circuits,” MIT Press, Cambridge, Massachusetts, Mass., 1987.
J. Krajicek, ∏1 -conservativeness in Systems of Bounded Arithmetic. Submitted.
J. Krajicek, Exponentiation and Second Order Bounded Arithmetic, Annals of Pure and Applied Logic (1989). To appear.
J. Krajíček-P. Pudlák, Quantified Propositional Calculus and Fragments of bounded Arithmetic, Zeitschr. f. Math. Logik (1988). To appear.
J. Krajicek-P. Pudlak-G. Takeuti, Bounded Arithmetic and the Polynomial Hierarchy, Annals of Pure and Applied Logic (1989). To appear.
A. Meyer-L. Stockmeyer, The Equivalence Problem for Regular Expressions with Squaring Requires Exponential Time, Proc. 13th IEEE Symp. on Switching and Automato Th. (1973), 125–129.
J. Paris-A. Wilkie, On the Scheme of Induction for Bounded Arithmetic Formulas, Annals of Pure and Applied Logic 35 (3) (1987), 205–303.
G. Takeuti, “Proof Theory,” North Holland, 1975. Second edition (1987).
G. Takeuti, Bounded Arithmetic and Truth Definition, Annals of Pure and Applied Logic 39 (1) (1988), 75–104.
G. Takeuti,, i3 and \(\mathop{{V_{2}^{i}}}\limits^{ \circ }\) ( BD ). Archive for Mathematical Logic (1990). To appear.
A. Yao, Separating the Polynomial-Time Hierarchy by Oracles Proceedings, 26th Annual IEEE Symposium on Foundations of Computer Science (1985), 1–10.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1990 Birkhäuser Boston
About this chapter
Cite this chapter
Krajíček, J., Takeuti, G. (1990). On Bounded ∑ 11 Polynomial Induction. In: Buss, S.R., Scott, P.J. (eds) Feasible Mathematics. Progress in Computer Science and Applied Logic, vol 9. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-3466-1_15
Download citation
DOI: https://doi.org/10.1007/978-1-4612-3466-1_15
Publisher Name: Birkhäuser Boston
Print ISBN: 978-0-8176-3483-4
Online ISBN: 978-1-4612-3466-1
eBook Packages: Springer Book Archive