Structure of complexity in the weak monadic second-order theories of the natural numbers

ABSTRACT

The complexity of decision procedures for the Weak Monadic Second-Order Theories of the Natural Numbers are considered. If only successor is allowed as a primitive, then every alternation of second-order quantifiers causes an exponential increase in the complexity of deciding the validity of a formula. Thus a heirarchy similar in form to Kleene's arithmetic heirarchy may be shown to correspond to the Ritchie functions. On the other hand, if first-order less-than is allowed as a primitive, one existential quantifier suffices for arbitrarily complex (in the Ritchie heirarchy) decision problems. This leads to a normal form, in which every sentence in the theory is equivalent in polynomial time to a sentence with less-than but only one existential second-order quantifier.

REFERENCES

• 1: Büchi, J.R. Weak second-order arithmetic and finite automata, Zeit Math. logik Grundl. Math. 6 (1960), 66-92.
• 2: Stephen A. Cook, The complexity of theorem-proving procedures, Proceedings of the third annual ACM symposium on Theory of computing, p.151-158, May 03-05, 1971, Shaker Heights, Ohio, United States [doi>10.1145/800157.805047]
• 3: Elgot, C.C. Decision problems of finite automata design and related arithmetics, Trans. AMS, 99 (1961), 21-51.
• 4: L. H. Landweber , E. L. Robertson, Recursive Properties of Abstract Complexity Classes, Journal of the ACM (JACM), v.19 n.2, p.296-308, April 1972 [doi>10.1145/321694.321702]
• 5: Lewis, F.D. The enumerability and invariance of complexity classes, JCSS 5, 3 (June 1971), 286-303.
• 6: A. R. Meyer, WEAK MONADIC SECOND ORDER THEORY OF SUCCESSOR IS NOT ELEMENTARY-RECURSIVE, Massachusetts Institute of Technology, Cambridge, MA, 1973
• 7: Meyer, A. R. and Stockmeyer, L.J. The equivalence problem for regular expressions with squaring requires exponential space, Proc. 13th Ann. IEEE Symp. on Switching and Automata Theory (Oct. 1972), 125-129.
• 8: Ritchie, R.W. Classes of predictably computable functions, Trans. AMS, 106 (1963), 139-173.
• 9: Robertson, E.L. Structure of complexity in the weak monadic second-order theories of the natural numbers, Research Report CS-73-31, Dept. of Applied Analysis and Computer Science, University of Waterloo, (Dec. 1973).

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.3 Complexity Measures and Classes
          Subjects: Relations among complexity classes

Additional Classification:
  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Bounded-action devices (e.g., Turing machines, random access machines)
  F.2 ANALYSIS OF ALGORITHMS AND PROBLEM COMPLEXITY
      F.2.1 Numerical Algorithms and Problems
          Subjects: Computations on polynomials
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.3 Formal Languages
          Subjects: Decision problems

General Terms:
Theory