Advertisement

Closure Properties of Weak Systems of Bounded Arithmetic

  • Antonina Kolokolova
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3634)

Abstract

In this paper we study the properties of systems of bounded arithmetic capturing small complexity classes and state conditions sufficient for such systems to capture the corresponding complexity class tightly. Our class of systems of bounded arithmetic is the class of second-order systems with comprehension axiom for a syntactically restricted class of formulas Φ ⊂ Σ\(_{\rm 1}^{B}\) based on a logic in the descriptive complexity setting. This work generalizes the results of [8] and [9].

We show that if the system 1) extends V 0 (second-order version of IΔ0), 2) Δ1-defines all functions with bitgraphs from Φ, and 3) proves witnessing for all theorems from Φ, then the class of Σ\(_{\rm 1}^{B}\)-definable functions of the resulting system is exactly the class expressed by Φ in the descriptive complexity setting, provably in this system.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Barrington, D.M., Immerman, N., Straubing, H.: On uniformity within NC1. Journal of Computer and System Sciences 41(3), 274–306 (1990)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Clote, P., Takeuti, G.: Bounded arithmetic for NC, ALOGTIME, L and NL. Annals of Pure and Applied Logic 56, 73–117 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Clote, P., Takeuti, G.: First order bounded arithmetic and small boolean circuit complexity classes. In: Feasible Mathematics, vol. II, Birkhäuser Inc., Basel (1995)Google Scholar
  4. 4.
    Cobham, A.: The intrinsic computational difficulty of functions. In: Bar-Hillel, Y. (ed.) Logic, Methodology and Philosophy of Science, Amsterdam, pp. 24–30. North-Holland, Amsterdam (1965)Google Scholar
  5. 5.
    Cook, S.: Theories for complexity classes and their propositional translations, pp. 1–36 (2004) (submitted)Google Scholar
  6. 6.
    Cook, S.A.: CSC 2429S: Proof Complexity and Bounded Arithmetic. Course notes (Spring 1998-2002), http://www.cs.toronto.edu/~sacook/csc2429h
  7. 7.
    Cook, S.A., Kolokolova, A.: A second-order system for polynomial-time reasoning based on Grädel’s theorem. In: Proceedings of the Sixteens annual IEEE symposium on Logic in Computer Science, pp. 177–186 (2001)Google Scholar
  8. 8.
    Cook, S.A., Kolokolova, A.: A second-order system for polytime reasoning based on Grädel’s theorem. Annals of Pure and Applied Logic 124, 193–231 (2003)zbMATHCrossRefMathSciNetGoogle Scholar
  9. 9.
    Cook, S.A., Kolokolova, A.: Bounded arithmetic of NL. In: Proceedings of the Nineteens annual IEEE symposium on Logic in Computer Science, pp. 398–407 (2004)Google Scholar
  10. 10.
    Cook, S., Thapen, N.: The strength of replacement in weak arithmetic. In: Proceedings of the Nineteens annual IEEE symposium on Logic in Computer Science, pp. 256–264 (2004)Google Scholar
  11. 11.
    Ebbinghaus, H.-D., Flum, J.: Finite model theory. Springer, Heidelberg (1995)zbMATHGoogle Scholar
  12. 12.
    Fagin, R.: Generalized first-order spectra and polynomial-time recognizable sets. In: Complexity of computation, SIAM-AMC proceedings, vol. 7, pp. 43–73 (1974)Google Scholar
  13. 13.
    Grädel, E.: The Expressive Power of Second Order Horn Logic. In: Jantzen, M., Choffrut, C. (eds.) STACS 1991. LNCS, vol. 480, pp. 466–477. Springer, Heidelberg (1991)CrossRefGoogle Scholar
  14. 14.
    Grädel, E.: Capturing Complexity Classes by Fragments of Second Order Logic. Theoretical Computer Science 101, 35–57 (1992)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Immerman, N.: Relational queries computable in polytime. In: 14th ACM Symp.on Theory of Computing, pp. 147–152. Springer, Heidelberg (1982)Google Scholar
  16. 16.
    Immerman, N.: Descriptive complexity. Springer, New York (1999)zbMATHGoogle Scholar
  17. 17.
    Kolokolova, A.: Systems of bounded arithmetic from descriptive complexity. PhD thesis, University of Toronto (October 2004)Google Scholar
  18. 18.
    Libkin, L.: Elements of Finite Model Theory. Springer, Heidelberg (2004)zbMATHGoogle Scholar
  19. 19.
    Nguyen, P., Cook, S.: Theories for TC0 and other small complexity classes (2004) (submitted)Google Scholar
  20. 20.
    Nisan, N., Ta-Shma, A.: Symmetric logspace is closed under complement. In: Proc. 27th Ann. ACM Symp. on Theory of Computing (STOC 1995), pp. 140–146 (1995)Google Scholar
  21. 21.
    Razborov, A.: An equivalence between second-order bounded domain bounded arithmetic and first-order bounded arithmetic. In: Clote, P., Krajiček, J. (eds.) Arithmetic, proof theory and computational complexity, pp. 247–277. Clarendon Press, Oxford (1993)Google Scholar
  22. 22.
    Reingold, O.: Undirected ST-Connectivity in Log-Space. Electronic Colloquium on Computational Complexity, ECCC Report TR04-094 (2004)Google Scholar
  23. 23.
    Schaefer, T.J.: The complexity of satisfiability problems. In: Proceedings of the Tenth Annual ACM Symposium on Theory of Computing, pp. 216–226 (1978)Google Scholar
  24. 24.
    Stockmeyer, L.J.: The polynomial-time hierarchy. Theoretical Computer Science 3, 1–22 (1977)zbMATHCrossRefMathSciNetGoogle Scholar
  25. 25.
    Takeuti, G.: RSUV isomorphism. In: Clote, P., Krajiček, J. (eds.) Arithmetic, proof theory and computational complexity, pp. 364–386. Clarendon Press, Oxford (1993)Google Scholar
  26. 26.
    Zambella, D.: Notes on polynomially bounded arithmetic. The Journal of Symbolic Logic 61(3), 942–966 (1996)zbMATHCrossRefMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Antonina Kolokolova
    • 1
  1. 1.Simon Fraser University & Mathematical InstitutePrague

Personalised recommendations