Hostname: page-component-586b7cd67f-tf8b9 Total loading time: 0 Render date: 2024-11-24T18:37:29.386Z Has data issue: false hasContentIssue false
  • English
  • Français

A theory for Log-Space and NLIN versus co-NLIN

Published online by Cambridge University Press:  12 March 2014

Chris Pollett
Chris Pollett*
Affiliation:
214 Macquarrie Hall, Department of Computer Science, San Jose State University, 1 Washington Square, San Jose CA 95192, USA, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

The use of Nepomnjaščiǐ's Theorem in the proofs of independence results for bounded arithmetic theories is investigated. Using this result and similar ideas, it is shown that at least one of S1 or TLS does not prove the Matiyasevich-Robinson-Davis-Putnam Theorem. It is also established that TLS does not prove a statement that roughly means nondeterministic linear time is equal to co-nondeterministic linear time. Here S1 is a conservative extension of the well-studied theory IΔ0 and TLS is a theory for LOGSPACE reasoning.

Keywords

bounded arithmeticindependence resultsMRDP
Type
Research Article
Information
The Journal of Symbolic Logic , Volume 68 , Issue 4 , December 2003 , pp. 1082 - 1090
Copyright
Copyright © Association for Symbolic Logic 2003

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, S. R., Bounded arithmetic, Bibliopolis, Napoli, 1986.Google Scholar
[2] Clote, P. and Takeuti, G., First order bounded arithmetic and small Boolean circuit complexity classes, Feasible mathematics, II (Clote, P. and Remmel, J., editors), Birkhäuser, Boston, 1995, pp. 154–218.Google Scholar
[3] Cook, S., A survey of complexity classes and their associated propositional proof systems and theories, and a proof system for Log Space, Slides for Edinburgh talk, presented at the ICMS Workshop “Circuit and Proof Complexity”, Edinburgh, 10, 2001.Google Scholar
[4] Ferreira, F., A proof that LOGSPACE ≠ NLIN, Unpublished notes, 1998.Google Scholar
[5] Fortnow, L., Time-space tradeoffs for satisfiability, Journal of Computer and System Sciences, vol. 60 (04 2000), no. 2, pp. 337–353.Google Scholar
[6] Gaifman, H. and Dimitracopoulos, C., Fragments of Peano's arithmetic and the MRDP theorem, Monographic de L'Enseignement Mathématique, vol. 30 (1982), pp. 187–206.Google Scholar
[7] Hájek, P. and Pudlák, P., Metamathematics of first-order arithmetic, Springer-Verlag, 1993.Google Scholar
[8] Johannsen, J. and Pollett, C., On the Δ1 b-comprehension rule, Logic colloquium 1998 (Buss, S., Hájek, P., and Pudlák, P., editors), Lecture Notes in Logic, vol. 13, A. K. Peters, 2000, pp. 269–286.Google Scholar
[9] Kent, C. F. and Hodgson, B. R., An arithmetical characterization of NP, Theoretical Computer Science, vol. 21 (1982), pp. 255–267.Google Scholar
[10] Krajíček, J., Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995.Google Scholar
[11] Matiyasevich, Y., Enumerable sets are Diophantine, Doklady Akademii Nauk, vol. 191 (1970), pp. 279–282.Google Scholar
[12] Nepom, V. A.., Rudimentary predicates and Turing computations, Doklady Akademii Nauk, vol. 195 (1970), pp. 282–284.Google Scholar
[13] Pollett, C., Nepom's theorem and independence proofs in bounded arithmetic, Technical Report TR02-051, Electronic Colloquium on Computational Complexity.Google Scholar
[14] Pollett, C., Structure and definability in general bounded arithmetic theories, Annals of Pure and Applied Logic, vol. 100 (1999), pp. 189–245.CrossRefGoogle Scholar
[15] Pollett, C., Multifunction algebras and the provability of PH ↓, Annals of Pure and Applied Logic, vol. 104 (2000), pp. 279–303.Google Scholar
[16] Pollett, C., Sk,exp does not prove NP = co-NP uniformly, Zapiski Nauchnykh Seminarov. Dom 1, vol. 304, 2003.Google Scholar
[17] Pollett, C. and Pruim, R., Strengths and weaknesses of LH arithmetic, Mathematical Logic Quarterly, vol. 48 (02 2002), no. 2, pp. 221–243.Google Scholar
[18] Takeuti, G., RSUV isomorphisms, Arithmetic, proof theory, and computational complexity (Clote, P. and Krajíček, J., editors), Oxford Logic Guides, vol. 23, Clarendon Press, Oxford, 1993, pp. 364–386.Google Scholar
[19] Takeuti, G., Frege proof system and TNC°, this Journal, vol. 63 (1998), no. 2, pp. 709–738.Google Scholar
[20] Wrathall, C., Rudimentary predicates and relative computation, SIAM Journal of Computing, vol. 7 (1978), pp. 194–209.CrossRefGoogle Scholar
[21] Zambella, D., End extensions of models of linearly bounded arithmetic, Annals of Pure and Applied Logic, vol. 88 (1997), no. 2-3, pp. 263–277.Google Scholar