# 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.2 Using Predicate Logic to Describe Problems  
Having a look at the list of problems, you will first notice that they are all graph problems. This already indicates a direction in which our logical description should go: First, to simplify matters, we will only consider graphs as inputs, which fits perfectly with the list of problems in the theorem (one can more generally consider arbitrary logical structures, but while this does not add expressive power, it does add unnecessary complications in the context of the present paper). Second, in order to talk about graphs using logic, we need to reference them in logical formulas. We do so by viewing a (directed) graph \(G=(V,E)\) with vertex set \(V\) and edge set \(E\subseteq V\times V\) as a logical structure \(\mathcal{G}=(V,E^{\mathcal{G}})\) in the sense of predicate logic with \"universe \(V^{\prime\prime}\) and \(E^{\mathcal{G}}=E\) being a binary relation on this universe. The signature (also sometimes called a logical vocabulary) of the structure is \(\tau_{\text{graphs}}=(E^{2})\), consisting of a single binary relation symbol. The (first-order) variables of a formula in predicate logic will now refer to vertices: Consider the simple problem of deciding whether all vertices of a graph have an outgoing edge. A graph \(\mathcal{G}=(V,E^{\mathcal{G}})\) will have this property if, and only if, \(\mathcal{G}\models\forall x\exists y\,E(x,y)\), that is, if it is a model of the formula. As another example, the problem of telling whether there is a walk of length 2 somewhere in the graph be expressed using the formula \(\exists x\exists y\exists z(E(x,y)\wedge E(y,z))\). In general, the set of all (finite) graph models of a formula is said to be the problem _described_ by the formula. Returning to the list of problems in the quotation, you may also have noticed that they lie in NP and are typically NP-complete. To describe such problems, formulas in first-order logic do not suffice: basically, each first-order quantifier in a formula can be \"tested\" using a simple parallel for-loop and, thus, first-order formulas can only describe rather simple problems. The great power of the class NP comes from the ability of nondeterministic Turing machines to \"guess\" not only a single vertex, but rather a whole set of vertices. For instance, an NP-machine for deciding the problem 3-colorable (decide whether a graph can be colored with three colors so that there are no monochromatic edges) will nondeterministically guess the three color sets and then do a simple test whether it has \"guessed correctly\". Translated to the logical setting, we wish to talk about (and guess) whole sets of vertices, which means using _second-order variables_: They work and behave like additional relational symbols, but they are not part of the signature. Rather, quantifying over them existentially corresponds exactly to guessing a set of vertices (or even a binary relation) using an NP-machine. As an example, we can express the problem 3-colorable using the following second-order formula \(\phi_{3\text{-colorable}}\):  
\[\exists R\exists G\exists B\forall x\Big{(}(R(x)\lor G(x)\lor B(x))\wedge\] \[\forall y\big{(}E(x,y)\rightarrow\big{(}\
eg(R(x)\wedge R(y)) \wedge\
eg(G(x)\wedge G(y))\wedge\
eg(B(x)\wedge B(y))\big{)}\big{)}\Big{)} \tag{1}\]  
Let us \"read this formula aloud\": it asks whether there exists a set \(R\) of (red) vertices, a set \(G\) of (green) vertices, and a set \(B\) of (blue) vertices such that all vertices \(x\) have one of these colors and for all edges \(E(x,y)\) the two endpoints \(x\) and \(y\) do not have the same color. As another example, let us express the problem graph-automorphism, which asks whether a graph \(G\) is isomorphic to itself via some isomorphism that is not the identity.