Structure of complexity in the weak monadic second-order theories of the natural numbers
Edward L. Robertson · 1974
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.