First-Order Closure and the Monadic Second-Order Alternation Hierarchy
The first-order closure of a class F of formulas is the smallest superclass of F that is closed under first-order quantification. We show some separation results concerning the first-order closure of different levels of the monadic second-order quantifier alternation hierarchy over grids or graphs. To do so, we consider sets of rectangular grids where the width is a function of the height. If such a set is definable in the first-order closure of the boolean closure of level k, then the corresponding function is at most (k+1)-fold exponential (this generalizes a result of Ajtai, Fagin, and Stockmeyer from k=1 to arbitrary k). Moreover, we prove that this bound is asymptotically optimal (this solves, for the case k=1, an open question of Ajtai, Fagin, and Stockmeyer).