Abstract
A well known result of proof theory is the characterization of primitive recursive functions ƒ as those provably recursive in the first order theory of Peano arithmetic with the induction axiom restricted to Σ1 formulas. In this paper, we study a variety of weak theories of first order arithmetic, whose provably total functions (with graphs of a certain form) are exactly those computable within some resource bound on a particular computation model (boolean circuits, with possible parity or MOD 6 gates, or threshold circuits, or alternating Turing machines, or ordinary Turing machines). To establish these kinds of results for small complexity classes, we provide a recursion-theoretic characterization of the complexity class, prove how one can encode sequences in very weak theories, and use the witnessing technique of [7].
Research partially supported by NSF INT-9014569 and CCR-9102896.
Research partially supported by NSF INT-9014569.
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
M. Ajtai. The complexity of the pigeon hole principle. In Proceedings of IEEE 29th Annual Symposium on Foundations of Computer Science, 1988. pp. 346 – 355.
M. Ajtai. Parity and the pigeonhole principle. In S.R. Buss and P.J. Scott, editors, Feasible Mathematics, pages 1–24. Birkhäuser, 1990.
B. Allen. Arithmetizing uniform NC. Annals of Pure and Applied Logic, 53 (1): 1 – 50, 1991.
D. Mix Barrington, N. Immerman, and H. Straubing. On uniformity in NC 1. J. Comp. Syst. Sci., 41(3):274–306, 1990. Preliminary version appeared in Structure in Complexity Theory: 3rd Annual Conference, IEEE Computer Society Press (1988), 47–59.
D.A. Barrington. Bounded-width polynomial-size branching programs recognize exactly those languages in nc 1. Journal of Computer and System Sciences, 38:150–164,1989. Preliminary version in Proceedings of the 18th Annual ACM Symposium on Theory of Computing(1986) 1–5.
P. Beame, R. Impagliazzo, J. Krajíček, T. Pitassi, P. Pudlák, and A. Woods. Exponential lower bounds for the pigeonhole principle. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing, Victoria, 1992.
S. Buss. Bounded Arithmetic, volume 3 of Studies in Proof Theory. Bibliopolis, 1986. 221 pages.
S. Buss. The propositional pigeonhole principle has polynomial size Frege proofs. Journal of Symbolic Logic, 52:916 – 927, 1987.
P. Clote. Arithmetic: Proof theory and model theory. MIT Lecture Notes, 1987.
P. Clote. A sequential programming language for parallel complexity classes. Technical Report BCCS-88-07, Boston College, Computer Science Department, November 1988.
P. Clote. A first order theory for the parallel complexity class NC. Technical Report BCCS-89-01, Boston College, Computer Science Department, January 1989.
P. Clote. ALOGTIMEand a conjecture of S.A. Cook. Annals of Mathematics and Artificial Intelligence, 6:57–106, 1992. extended abstract in proceedings of IEEE Logic in Computer Science, Philadelphia, June 1990.
P. Clote. Polynomial size frege proofs of certain combinatorial principles. In P. Clote and J. Krajíček, editors, Arithmetic, Proof Theory and Computational Complexity, pages 162 – 184. Oxford University Press, 1993.
P. Clote and E. Kranakis. Boolean functions, parallel computation and proof systems. Monograph in preparation.
P. Clote and G. Takeuti. Bounded arithmetics for NC, ALOGTIME, Land NL. Annals of Pure and Applied Logic, 56: 73 – 117, 1992.
P. Clote and G. Takeuti. Bounded arithmetic and very fast parallel time. Typeset manuscript, July 24, 1990.
P.G. Clote. Sequential, machine-independent characterizations of the parallel complexity classes ALOGTIME, AC k , NC kand NC. In P.J. Scott S.R. Buss, editor, Feasible Mathematics, pages 49–70. Birkhäuser, 1990.
A. Cobham. The intrinsic computational difficulty of functions. In Y. Bar-Hillel, editor, Logic, Methodology and Philosophy of Science II, pages 24–30. North-Holland, 1965.
S.A. Cook. A taxonomy of problems with fast parallel algorithms. Information and Control, 64: 2 – 22, 1985.
W. Handley, J. B. Paris, and A. J. Wilkie. Characterizing some low arithmetic classes. In Theory of Algorithms, pages 353 – 364. Akademie Kyado, Budapest, 1984. Colloquia Societatis Janos Bolyai.
J.E. Hopcroft and J.D. Ullman. Introduction to Automata Theory. Addison-Wesley, 1979.
N. Immerman. Expressibility and parallel complexity. SIAM J. Cornput., 18 (3): 625 – 638, 1989.
J.C. Lind. Computing in logarithmic space. Technical Report Project MAC Technical Memorandum 52, Massachusetts Institute of Technology, September 1974.
G. Takeuti. A second order version of S 12 and U 12 Journal of Symbolic Logic, 56 (3): 1038 – 1063, 1991.
G. Takeuti. RSUVisomorphism. In P. Clote and J. Krajíček, editors, Arithmetic, Proof Theory and Computational Complexity, pages 364–386. Oxford University Press, 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1995 Birkhäuser Boston
About this paper
Cite this paper
Clote, P., Takeuti, G. (1995). First Order Bounded Arithmetic and Small Boolean Circuit Complexity Classes. In: Clote, P., Remmel, J.B. (eds) Feasible Mathematics II. Progress in Computer Science and Applied Logic, vol 13. Birkhäuser Boston. https://doi.org/10.1007/978-1-4612-2566-9_6
Download citation
DOI: https://doi.org/10.1007/978-1-4612-2566-9_6
Publisher Name: Birkhäuser Boston
Print ISBN: 978-1-4612-7582-4
Online ISBN: 978-1-4612-2566-9
eBook Packages: Springer Book Archive