On the existence of normal forms for logics that capture complexity classes
Argimiro Arratia · 1997
We show that the logic HEX$\sp*$ (FO$\sb{s}$), which is first-order logic (with successor) extended with a generalized quantifier (HEX) corresponding to the PSPACE-complete problem Generalized Hex, has a projective normal form. This gives as a corollary that HEX$\sp*$ (FO$\sb{s}$) captures PSPACE and that the problem Generalized Hex is complete via first-order projections. We define a variation of HEX, namely WHEX, and prove that as a problem (class of finite structures) it is also complete for PSPACE via logspace reducibility. Considering WHEX as a generalized quantifier, we form the logic WHEX$\sp*$ (FO$\sb{s}$) and show that it has similar properties as HEX$\sp*$ (FO$\sb{s}$); that is, it has a projective normal form and captures PSPACE; hence, WHEX is complete for PSPACE via first-order projections. Furthermore, we show that WHEX$\sp*$ (FO$\sb{s}$) is contained in the infinitary logic L$\sbsp{\infty\omega}{\omega}$. We then study the existence of normal forms for the logics HEX$\sp*$ (FO) and WHEX$\sp*$ (FO), where the successor relation is not present, and conclude that they have no projective normal forms. In fact, we prove a general theorem that states the non-existence of a projective normal form for various extensions of first-order logic (without successor) of the form $\Omega\sp*$ (FO), when $\Omega$ is a generalized quantifier that corresponds to a firmly monotone problem. The tool we employ for obtaining our negative results is Ehrenfeucht-Fraisse games for logics with generalized quantifiers. We continue our explorations in the world of unordered structures with a revision of a theorem by Gradel, which states the existence of a hierarchy of logics inside Transitive Closure logic, or TC$\sp*$ (FO). We translate this result to the framework of program schemes, and obtain a hierarchy of certain classes of program schemes. Our Hierarchy Theorem for program schemes generalizes Gradel's Hierarchy Theorem for TC$\sp*$ (FO), since, as we show, his theorem can be obtained as a corollary from ours, and similar hierarchies inside other logics of the form $\Omega\sp*$ (FO), where $\Omega$ is a generalized quantifier of complexity within NL, are also consequences of our theorem.