# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 3 An Algorithmic Metatheorem for Logspace and Its Applications
### Applications: High-Hanging Fruits II--A Refined Version of Fagin's Theorem  
I mentioned Fagin's Theorem already as one of the cornerstones of descriptive complexity theory: it states that a problem lies in NP if, and only if, it can be described in _existential second-order_ logic (eso-logic). Recall that this logic differs from monadic second-order logic in two ways: we _can_ quantify over binary relations and not only over sets of vertices (which is why the formula describingthe graph automorphism problem is allowed), but we can _not_ quantify universally. This means that all ESO-formulas can be rewritten equivalently in \"prenex normal form\", which, in turn, means that they are of the form \(\exists R_{1}\cdots\exists R_{n}\forall x_{1}\exists x_{2}\forall x_{3}\cdots \exists x_{n}\psi\) for some quantifier-free \(\psi\), some second-order variables \(R_{i}\) (not necessarily monadic), and some first-order variables \(x_{i}\). Formulas like \(\phi_{3\text{-colorable}}\) from the introduction show that already fragments of ESO-logic describe NP-complete problems, in this case a formula with the quantifier prefix \(\exists\mathtt{R}\mathtt{R}\mathtt{G}\mathtt{B}\Psi\mathtt{x}\forall y\). Is this still the case for a shorter prefix like, say, \(\exists\mathtt{X}\exists Y\forall x\forall y\)? The answer is \"yes\" since, using two quantifiers (\(\exists\mathtt{X}\) and \(\exists\mathtt{Y}\)), we can \"guess\" two bits of information for each vertex of a graph, and two bits suffice to describe which of three (even four) possible colors a vertex has. In other words, the quantifier prefix \(\exists\mathtt{X}\exists Y\forall x\forall y\) can be used to describe the NP-complete problem 4-colorable. Thus, what about the prefix \(\exists\mathtt{X}\forall x\forall y\)? By the same argument, we can describe the 2-colorability problem in this logic, but this is presumably no longer an NP-complete problem, but an L-complete problem. Indeed, it turns out that _all_ problems that can be described by formulas with this prefix already lie in _nondeterministic logarithmic space_ (NL), which is a (presumably small) subclass of P. Naturally, this observation opens a whole box of new questions regarding the expressive power of all the possible quantifier prefixes an ESO-formula may have. Extensive research regarding the expressive power of different quantifier prefixes has climaxed in a 51-page paper [19] in the Journal of the ACM by [PERSON], [PERSON], and [PERSON] where a dichotomy is proved: for each possible ESO quantifier prefix, it is shown that the corresponding _prefix class_ (the class of problems expressible by formulas having the given quantifier prefix) either contains an NP-complete problem or is contained in P.  
While the NP-hardness results can be obtained by fairly easy reductions from standard problems, the containment results for P are more involved. Indeed, for one particular prefix class, showing containment in P is very difficult: [PERSON], [PERSON], and [PERSON] [19] spend most of their paper on showing that for all formulas \(\phi\) of the form \(\exists R_{1}\cdots\exists R_{n}\,\forall x\exists y\,\psi\), where \(\psi\) is quantifier-free, the language \(L_{\phi}=\{\mathcal{G}\mid\mathcal{G}\text{ is an {undirected}, self-loop-free}\text{ graph with }\mathcal{G}\models\phi\}\) lies in P. The authors already observe that their result is probably not the best possible: the languages \(L_{\phi}\) equal a special problem \"\(SATU(P)\)\" in their terminology, and, in their Remark 5.1, they observe \"Note also that for each \(P\), \(SATU(P)\) is probably not a PTIME-complete set. [...] This is due to the check for bounded tree width, which is in LOGCFL (cf. [PERSON] [1994]) but not known to be in NL\". As this remark shows, the complexity of the prefix class hinges critically on computing tree decompositions.