Arity and alternation in second-order logic Original Research Article

We investigate the expressive power of second-order logic over finite structures, when two limitations are imposed. Let SAA(k, n)(AA(k, n)) be the set of second-order formulas such that the arity of the relation variables is bounded by k and the number of alternations of (both first-order and) second-order quantification is bounded by n. We show that this imposes a proper hierarchy on second-order logic, i.e. for every k, n there are problems not definable in AA(k, n) but definable in AA(k + c1, n + d1) for some c1, d1. The method to show this is to introduce the set AUTOSAT(F) of formulas in F which satisfy themselves. We study the complexity of this set for various fragments of second-order loeic. For first-order logic FOL with unbounded alternation of quantifiers AUTOSAT(FOL) is PSpacecomplete. For first-order logic FOLn with alternation of quantifiers bounded by n, AUTOSAT(FOLn) is definable in AA(3, n + 4). AUTOSAT(AA(k, n)) is definable in AA(k + c1,n + d1) for some c1, d1.