# On the Descriptive Complexity of Color Coding +
## 4 Syntactic Proofs and Natural Problems
### Bounded Strong-Rank Description of Model Checking for First-Order Logic  
An important result by [PERSON] and [PERSON] [10] states that the model checking problem for first-order logic lies in FPT on structures whose Gaifman graph has bounded degree (the Gaifman graph of a logical structure has the structure's universe as its vertex set and has an undirected edge between two vertices \(u\) and \(v\) if \(u\) and \(v\) are simultaneously part of some tuple of some relation of the structure; in particular, the Gaifman graph of a directed graph is its underlying undirected graph). Once more, this result can now be obtained \"syntactically.\" For simplicity, we only consider graphs and let  
\[ \begin{split}\mathbb{P}_{\psi,\delta^{-}\text{MC}}(\text{FO})=\big{\{} (\mathcal{G},\text{num}(\psi,\delta))&\big{|}\,\mathcal{G}\in \textsc{struc}[(E^{2})],\ \psi\in\text{FO},\\ &\mathcal{G}\models\psi,\text{max-degree}(\mathcal{G})\leq\delta \big{\}}.\end{split} \]  
**Theorem 7** ([7, 10]). : \(\mathbb{P}_{\psi,\delta^{-}\text{MC}}(\text{FO})\in\text{para-AC}^{0\dagger}\)_._  
Proof. : We present a family \((\phi_{\psi,\delta})_{\psi\in\text{FO},\delta\in\mathbb{N}}\) with a bound on the number of strong variables that describes \(\mathbb{P}_{\psi,\delta^{-}\text{MC}}(\text{FO})\). Fix \(\psi\) and \(\delta\). Recall that we fixed the signature for \(\psi\) to just \(\tau=(E^{2})\) for simplicity and, thus, \(\tau\)-structures are just graphs \(\mathcal{G}\). In particular, there are no arithmetic predicates available to \(\psi\) (one could, of course, also consider them, but then the Gaifman graph would always be a clique and the claim of the theorem would be boring). In contrast, the \(\phi_{\psi,\delta}\) are normal \(\text{FO}[+,\times]\) formulas and they have access to arithmetics. For a graph \(\mathcal{G}\) let us write \(\mathcal{G}\) for the underlying undirected graph and let us write \(\mathit{E}xy\) as a shorthand for \(\mathit{E}xy\lor\mathit{E}yx\). The first thing we check is that the maximum degree of the input graph \(\mathcal{G}\) is, indeed, \(\delta\). This is rather easy: \(\forall x2^{\leq\leq\delta}y(\mathit{E}xy)\). For the hard part of determining whether \(\mathcal{G}\models\psi\), let \(\bar{d}(a,b)\) denote the distance of two vertices in \(\mathcal{G}\) and let \(N_{r}(a)=\big{\{}b\in|\mathcal{G}|\ \big{|}\ \bar{d}(a,b)\leq r\big{\}}\) be the ball around \(a\) of radius \(r\) in \(\mathcal{G}\). Let \(\mathcal{G}[N_{r}(a)]\) denote the subgraph of \(\mathcal{G}\) induced on \(N_{r}(a)\). By Gaifman's Theorem [21] we can rewrite \(\psi\) as a Boolean combination of formulas of the following form:  
\[\exists x_{1}\cdots\exists x_{k}\Big{(} \bigwedge_{i\
eq j}\gamma_{\bar{d}(x_{i},x_{j})>2r}\wedge \tag{27}\] \[\bigwedge_{i}\rho(x_{i})\Big{)} \tag{28}\]  
where \(\gamma_{\bar{d}(x_{i},x_{j})>2r}\) expresses that \(\bar{d}(x_{i},x_{j})>2r\) should hold and \(\rho\) is \(r\)-local, meaning that for all \(a\in|\mathcal{G}|\) we have \(\mathcal{G}\models\rho(a)\iff\mathcal{G}[N_{r}(a)]\models\rho(a)\) (the minimum number \(r\) for which is the case is called the locality rank of \(\rho\)). We now wish to express the above formula using only a constant number of strong variables. The problem is, of course, that the \(x_{i}\) are not (yet) weak since they are used many times. We fix this in two steps. First, let us tackle (27): Clearly, the \(x_{i}\) will have a pairwise distance of at least \(2r\), if the balls of radius \(r\) that surround them are pairwise disjoint. Now, because of the bounded degree of the graph, a ball of radius \(r\) can have maximum size \(\delta^{r}\). This allows us to bind all members of each ball and testing disjointness is exactly what weak variables are all about. In detail, let \(\gamma_{\bar{d}(x,y)\leq r}\) be the standard formula with two bound variables expressing that there is path from \(x\) to \(y\) of length at most \(r\) in \(\mathcal{G}\).