Hostname: page-component-cd9895bd7-dk4vv Total loading time: 0 Render date: 2024-12-27T19:21:39.479Z Has data issue: false hasContentIssue false
  • English
  • Français

Double-exponential inseparability of Robinson subsystem Q+

Published online by Cambridge University Press:  12 March 2014

Lavinia Egidi  and
Giovanni Faglia
Lavinia Egidi
Affiliation:
Dipartimento di Informatica, Università del Piemonte Orientale “A. Avogadro”, Viale T. Michel, 11, 15121 Alessandria, Italy, E-mail: [email protected]
Giovanni Faglia
Affiliation:
Dipartimento di Informatica, Università del Piemonte Orientale “A. Avogadro”, Viale T. Michel, 11, 15121 Alessandria, Italy, E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this work a double exponential time inseparability result is proven for a finitely axiomatizable first order theory Q+. The theory, subset of Presburger theory of addition S+, is the additive fragment of Robinson system Q. We prove that every set that separates Q+ from the logically false sentences of addition is not recognizable by any Turing machine working in double exponential time. The lower bound is given both in the non-deterministic and in the linear alternating time models.

The result implies also that any theory of addition that is consistent with Q+—in particular any theory contained in S+—is at least double exponential time difficult. Our inseparability result is an improvement on the known lower bounds for arithmetic theories.

Our proof uses a refinement and adaptation of the technique that Fischer and Rabin used to prove the difficulty of S+. Our version of the technique can be applied to any incomplete finitely axiomatizable system in which all of the necessary properties of addition are provable.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 76 , Issue 1 , March 2011 , pp. 94 - 124
Copyright
Copyright © Association for Symbolic Logic 2011

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

[BDG90] Balcázar, José Luis, Diaz, Josep, and Gabarró, Joaquim, Structural complexity II, Springer-Verlag, 1990.CrossRefGoogle Scholar
[BS69] Bell, J.L. and Slomson, A.B., Models and ultraproducts, North-Holland, 1969.Google Scholar
[Ber80] Berman, Leonard, The complexity of logical theories, Theoretical Computer Science, vol. 11 (1980), pp. 71–77.CrossRefGoogle Scholar
[CH90] Compton, Kevin J. and Henson, C. Ward, A uniform method for proving lower bounds on the computational complexity of logical theories, Annals of Pure and Applied Logic, vol. 48 (1990), pp. 1–79.CrossRefGoogle Scholar
[Fag93a] Faglia, G., Double exponential inseparability of theories of addition, Ph.D. thesis, Università di Torino e Milano, Via Comelico 39, I-20135 Milano MI, Italy, 02 1993, In Italian.Google Scholar
[Fag93b] Faglia, G., Double exponential inseparability of Robinson subsystem Q+ from the unsatisfiable in the language of addition, Computational logic and proof theory, Third Kurt Gödel Colloquium, KGC'93, 1993, pp. 184–186.CrossRefGoogle Scholar
[FY92] Faglia, G. and Young, P., On the meaning of essentially unprovable theorems in the Presburger theory of addition, Theoretical computer science – Proceedings of the 4th Italian conference, World Scientific Publishing, 1992, pp. 214–228.Google Scholar
[FR75] Ferrante, Jeanne and Rackoff, Charles, A decision procedure for the first order theory of real addition with order, SIAM Journal of Computing, vol. 4 (1975), pp. 69–76.CrossRefGoogle Scholar
[FR79] Ferrante, Jeanne and Rackoff, Charles, The computational complexity of logical theories, Lecture Notes in Mathematics, vol. 718, Springer, 1979.CrossRefGoogle Scholar
[FR74] Fischer, M. J. and Rabin, M., Super-exponential complexity of Presburger arithmetic, Complexity of computation (Karp, R. M., editor), SIAM-AMS proceedings, vol. 7, American Mathematical Society, 1974, pp. 27–42.Google Scholar
[HB34] Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. 1, Springer, 1934.Google Scholar
[HU79] Hopcroft, John E. and Ullman, Jeffrey D., Introduction to automata theory, languages, and computation, Addison Wesley, 1979.Google Scholar
[MY78] Machtey, M. and Young, P., An introduction to the general theory of algorithms, Elsevier, 1978.Google Scholar
[Men87] Mendelson, Elliott, Introduction to mathematical logic, third ed., Mathematics Series, Wadsworth & Brooks/Cole Advanced Books & Software, Monterey, California, 1987.CrossRefGoogle Scholar
[Opp78] Oppen, Derek C., A 222pn upper bound on the complexity of Presburger arithmetic, Journal of Computer and System Sciences, vol. 16 (1978), pp. 323–332.CrossRefGoogle Scholar
[Pre29] Presburger, M., Über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. Comptes-rendus du I Congrès des Mathématiciens des Pays Slavs, 1929, pp. 92–101.Google Scholar
[Rob50] Robinson, Raphael M., An essentially undecidable axiom system, Proceedings of the International Congress of Mathematicians (Cambridge), vol. 1, 1950, pp. 729–30.Google Scholar
[Sto87] Stockmeyer, Larry, Classifying the computational complexity of problems, this Journal, vol. 52 (1987), no. 1, pp. 1–42.Google Scholar
[TMR53] Tarski, A., Mostowski, A., and Robinson, R., Undecidable theories, North-Holland, 1953.Google Scholar
[You85] Young, Paul, Gödel theorems, exponential difficulty and undecidability of arithmetic theories: An exposition, Recursion theory (Nerode, Anil and Shore, Richard A., editors), Proceedings of Symposia in Pure Mathematics, vol. 42, American Mathematical Society, 1985, pp. 503–522.CrossRefGoogle Scholar