# A Gentle Introduction to Applications of Algorithmic Metatheorems for Space and Circuit Classes
## 2 The Concepts and Ideas Behind Courcelle's Theorem
### Describing The Problems: Monadic Second-Order Logic
#### 2.1.3 The Need for _Monadic_ Predicates  
In view of [PERSON]'s Theorem and the list of problems in the cited theorem by [PERSON], \"existential second-order logic\" seems like a promising candidate for the logic that unifies all of the problems in the theorem. However, it turns out that this logic is not quite what we are looking for.  
To see where the problem lies, recall what our student did in the divide-and-conquer approach during the merging phase: Given solutions for the different subtrees of a tree, she devised a way of assembling them into an overall solution. The reason she could do this was that in order to combine several solutions for the subtrees, it only mattered _whether or not the roots of these subtrees were part of the optimal vertex cover or not_. In other words, there is only a small \"interface\" between the subtrees that is relevant for the vertex cover problem: the roots. The structure of the solution below the roots can be \"forgotten\" during the algorithm and has no influence on how the solutions to the subtrees are to be assembled optimally.  
Translated into the logical setting, we must be able to check the formula separately on subtrees \(T_{1}\) to \(T_{m}\) and then merge the results into an overall result. Vitally, during the merge, no vertices other than the roots may be of importance. In particular, we cannot test whether certain parts of the trees below the roots match or have some other similarity.  
[PERSON] observed that it is exactly the _non-monadic second-order variables_ that cause problems. A _monadic_ (or \"unary\") second-order variable stands for a set of vertices, while a binary second-order variable represents a second edge set. The difference is illustrated nicely by the two examples from above: for 3-COLORABLE, we only use monadic second-order variables and, indeed, if we have colorings for subtrees, merging them only requires us to look at the colors of the roots (of course, the 3-colorability problem is not very interesting for trees, but will become so for tree-like graphs in the next section). In stark contrast, for the graph automorphism problem, where our formula \"guessed\" the isomorphism using a binary predicate, we cannot merge automorphisms for the subtrees since the important question is exactly how the inner structures of these trees are related. Indeed, algorithmic metatheorems generally fail to apply to auto- and isomorphism problems even though these problems are not even believed to be NP-hard.  
To sum up, the logic we have been looking for is _monadic second-order logic over graphs_. We fix the signature to \(\tau_{\text{graphs}}=(E^{2},P^{1}_{1},\ldots,P^{1}_{m})\), where the \(P_{i}\) are optional predicate symbols that can be used to encode additional information about the vertices as part of the input. The formulas are first-order predicate logic formulas in which we may additionally quantify over _monadic predicate variables_ and use them as if they were unary relation symbols in the signature (in addition to the \(P_{i}\), over which we may _not_ quantify). We may quantify both existentially and universally (unlike Fagin's Theorem, where only existential quantification is allowed). The earlier formula for the 3-colorability problem is a typical example of a monadic second-order formula while the formula for the automorphism problem is not.