Hostname: page-component-586b7cd67f-rcrh6 Total loading time: 0 Render date: 2024-11-24T21:35:02.041Z Has data issue: false hasContentIssue false
  • English
  • Français

Delineating classes of computational complexity via second order theories with weak set existence principles. I

Published online by Cambridge University Press:  12 March 2014

Aleksandar Ignjatović
Aleksandar Ignjatović*
Affiliation:
Department of Philosophy, Carnegie Mellon University, Pittsburgh, Pennsylvania 15213, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we characterize the well-known computational complexity classes of the polynomial time hierarchy as classes of provably recursive functions (with graphs of suitable bounded complexity) of some second order theories with weak comprehension axiom schemas but without any induction schemas (Theorem 6). We also find a natural relationship between our theories and the theories of bounded arithmetic (Lemmas 4 and 5). Our proofs use a technique which enables us to “speed up” induction without increasing the bounded complexity of the induction formulas. This technique is also used to obtain an interpretability result for the theories of bounded arithmetic (Theorem 4).

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 60 , Issue 1 , March 1995 , pp. 103 - 121
Copyright
Copyright © Association for Symbolic Logic 1995

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Buss, Samuel R., Bounded arithmetic, Bibliopolis, Naples, 1986.Google Scholar
[2]Buss, Samuel R. and Ignjatović, Aleksandar, Unprovability of consistency statements in fragments of bounded arithmetic, Technical Report CMU-PHIL-43, Carnegie-Mellon University, Department of Philosophy, Pittsburgh, Pennsylvania, 01 1994; Annals of Pure and Applied Logic (to appear).Google Scholar
[3]Cook, Stephen, Feasibly constructive proofs and the propositional calculus, Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, New York, 1975, pp. 83–97.Google Scholar
[4]Ferreira, Fernando J. I., Polynomial time computable arithmetic, Logic and computation (Sieg, W., editor), Contemporary Mathematics, vol 106, American Mathematical Society, Providence, Rhode Island, 1990, pp. 137–156.CrossRefGoogle Scholar
[5]Ferreira, Fernando J. I., Polynomial time computable arithmetic and conservative extensions, Ph.D. thesis, Penn-sylvania State University, University Park, Pennsylvania, 1988.Google Scholar
[6]Ferreira, Fernando J. I., Stockmeyer induction, Feasible Mathematics (Buss, S. R. and Scott, P. J., editors), Proceedings of the Mathematical Sciences Institute workshop, Ithaca, New York, 06 1989, Birkhäuser, Boston, Massachusetts, 1990, pp. 161–180.CrossRefGoogle Scholar
[7]Hájek, P. and Pudlák, P., Metamathematics of first-order arithmetic, Springer-Verlag, Berlin, 1992.Google Scholar
[8]Ignjatović, Aleksandar, Delineating classes of computational complexity via second order theories with weak set existence principles. I, Technical report CMU-PHIL-22, Department of Philosophy, Carnegie-Mellon University, Pittsburgh, Pennsylvania, 11 1991.Google Scholar
[9]Ignjatović, Aleksandar, Induction in theories of bounded arithmetic, manuscript in preparation.Google Scholar
[10]Ignjatović, Aleksandar and Sieg, Wilfried, Herbrand analysis of some theories with weak set existence principles, manuscript in preparation.Google Scholar
[11]Leivant, Daniel, A foundational delineation of computational feasibility, draft (07 1991).Google Scholar
[12]Pudlák, Pavel, A note on bounded arithmetic, Fundamenta Mathematicae, vol. 136 (1990), pp. 85–89.CrossRefGoogle Scholar
[13]Solovay, Robert, Letter to P. Hájek, August 1976.Google Scholar