Arity and alternation in second-order logic (Q1919768)

This paper studies the expressiveness of second-order logic over finite structures. Two hierarchies of second-order formulas are introduced. In the \(\text{AA} (k,n)\) hierarchy the arity of any relation variable is \(\leq k\) and the number of alternations of quantifiers (first or second order) is \(\leq n\). In the \(\text{SAA} (k,n)\) hierarchy all second-order quantifiers come first and the first-order quantifiers are ignored in the alternation count. It is proven that for every \(k\), \(n \in N\) there are problems not definable in \(\text{AA} (k,n)\) but definable in \(\text{AA} (k + c_1, \;n + d_1)\) for some \(c_1\), \(d_1 \in N\). The method of proof involves the introduction of \(\text{AUTOSAT}(F)\), a set of formulas of the fragment of second-order logic \(F\) which satisfy themselves. The authors investigate the complexity of \(\text{AUTOSAT} (F)\) for various \(F\). For example they show that \(\text{AUTOSAT} (FOL)\) is PSpace-complete and for every \(k\), \(n \in N\) \(\text{AUTO(SAA} (k,n))\) is PSpace-complete.