Double-exponential inseparability of Robinson subsystem \(Q_{+}\). (English) Zbl 1222.03033

Summary: In this work a double exponential time inseparability result is proven for a finitely axiomatizable first-order theory \(Q_{+}\). The theory, a subset of the Presburger theory of addition \(S_{+}\), is the additive fragment of Robinson’s 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 nondeterministic 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.


03C07 Basic properties of first-order languages and structures
03D15 Complexity of computation (including implicit computational complexity)
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Full Text: DOI


[1] DOI: 10.1090/pspum/042/791074
[2] Complexity of computation 7 pp 27– (1974)
[3] DOI: 10.1137/0204006 · Zbl 0294.02022
[4] Theoretical computer science – Proceedings of the 4th Italian conference pp 214– (1992)
[5] Computational logic and proof theory pp 184– (1993)
[6] DOI: 10.1016/0168-0072(90)90080-L · Zbl 0705.03017
[7] DOI: 10.1016/0304-3975(80)90037-7 · Zbl 0475.03017
[8] Models and ultraproducts (1969) · Zbl 0179.31402
[9] Structural complexity II (1990) · Zbl 0746.68032
[10] Undecidable theories (1953)
[11] Classifying the computational complexity of problems 52 pp 1– (1987) · Zbl 0639.03041
[12] Proceedings of the International Congress of Mathematicians 1 pp 729– (1950)
[13] Comptes-rendus du I Congrès des Mathématiciens des Pays Slavs pp 92– (1929)
[14] DOI: 10.1016/0022-0000(78)90021-1 · Zbl 0381.03021
[15] Introduction to mathematical logic (1987)
[16] An introduction to the general theory of algorithms (1978)
[17] Introduction to automata theory, languages, and computation (1979) · Zbl 0426.68001
[18] Grundlagen der Mathematik 1 (1934) · JFM 60.0017.02
[19] The computational complexity of logical theories 718 (1979) · Zbl 0404.03028
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.