A restricted second order logic for finite structures

Reviewer: Anil Seth

In recent years, finite variable infinitary logic (\lw) has received a great deal of attention in finite model theory. Popular logics such as least fixed point logic (LFP) and partial fixed point logic (PFP), which correspond (on ordered structures) to complexity classes P and PSPACE respectively, are known to be fragments of \lw. In this paper the author shows a way to restrict the second order quantification in the definition of second order logic, to obtain analogues of NP and other levels of the polynomial hierarchy within finite variable logic. The definition of restricted second order logic (denoted $SO^{\omega}$) though clean is not completely elementary as it uses the technical notion of the $k$-equivalence relation, $\equiv^k$, as primitive. The motivation of defining these logics is to understand about different fragments of \lw and to apply some techniques of finite variable logics to these new fragments. The logic corresponding to NP obtained in this way (denoted $\Sigma^{1,\omega}_{1}$) is shown to be the same as nondeterministic fixed point logic (NFP), a fixed point analog of NP, introduced by Abiteboul and Vianu, thus demonstrating robustness of the $SO^{\omega}$. Further, it is shown that levels of $SO^{\omega}$ and fixed point logics (such as LFP, PFP) are the same over finite structures iff the corresponding complexity classes coincide, thus obtaining logical counterparts for more complexity theoretic statements. Some natural NP-complete problems, such as UFI (Unary NFA inequivalence), are shown to be expressible in $\Sigma^{1,\omega}_{1}$. This has an interesting corollary, that a specific problem (for example, UFI) is expressible in LFP iff P=NP. The paper closes with a gem of a proof showing that 3-colorability is not expressible in \lw. The proof builds on the work of Cai, Furer and Immerman and uses some clever ideas to settle this open problem. Finally, the paper is very well written and achieves great clarity, fluency and precision at the same time which makes it a pleasure to read. It should be accessible, informative and enjoyable reading for anyone who has had a first course in finite model theory.