# On the Descriptive Complexity of Color Coding +
## 3 Syntactic Properties Allowing Color Coding
### Formulas with Color Predicates  
In graph theory, a coloring of a graph can either refer to an arbitrary assignment that maps each vertex to a color or to such an assignment in which vertices connected by an edge must get different colors (sometimes called proper colorings). For our purposes, colorings need not be proper and are thus partitions of the vertex set into color classes. From the logical point of view, each color class can be represented by a unary predicate. A \(k\)-coloring of a \(\tau\)-structure \(\mathcal{A}\) is a structure \(\mathcal{B}\) over the signature \(\tau_{k\text{-colors}}=\tau\cup\{C_{1}^{1},\ldots,C_{k}^{1}\}\), where the \(C_{i}\) are fresh unary relation symbols, such that \(\mathcal{A}\) is the \(\tau\)-restriction of \(\mathcal{B}\) and such that the sets \(C_{1}^{\mathcal{B}}\) to \(C_{k}^{\mathcal{B}}\) form a partition of the universe \(|\mathcal{A}|\) of \(\mathcal{A}\). Let us now formulate and prove the first syntactic version of color coding. An example of a possible formula \(\phi\) in the below theorem is \(\bigwedge_{i=1}^{k}\exists x\exists y\exists z(Exy\wedge Eyz\wedge Exz\wedge C_{ i}x\wedge C_{i}y\wedge C_{i}z)\), for which the theorem tells us that there is a formula \(\phi^{\prime}\) of constant quantifier rank that is true exactly when there are pairwise disjoint sets \(C_{i}\) that make \(\phi\) true. Theorem 3.2: _Let \(\tau\) be an arithmetic signature and let \(k\) be a number. For each first-order \(\tau_{k\text{-colors}}\)-sentence \(\phi\) in negation normal form in which no \(C_{i}\) is inside a universal scope, there is a \(\tau\)-sentence \(\phi^{\prime}\) such that:_  
1. _For all_ \(\mathcal{A}\in\textsc{struc}[\tau]\) _we have_ \(\mathcal{A}\models\phi^{\prime}\) _if and only if there is a_ \(k\)_-coloring_ \(\mathcal{B}\) _of_ \(\mathcal{A}\) _with_ \(\mathcal{B}\models\phi\)_._
2. \(\operatorname{qr}(\phi^{\prime})=\operatorname{qr}(\phi)+O(1)\)_._
3. \(|\operatorname{bound}(\phi^{\prime})|=|\operatorname{bound}(\phi)|+O(1)\)_._ (Let us clarify that_ \(O(1)\) _represents a global constant that is independent of_ \(\tau\) _and_ \(k\)_. )_  
Proof. : Let \(\tau\), \(k\), and \(\phi\) be given as stated in the theorem. If necessary, we modify \(\phi\) to ensure that there is no literal of the form \(\
eg C_{i}x_{j}\), by replacing each such literal by the equivalent \(\bigvee_{i\
eq i}C_{i}x_{j}\). After this transformation, the \(C_{i}\) in \(\phi\) are neither in the scope of universal quantifiers nor of negations--and this is also true for all subformulas \(\alpha\) of \(\phi\). We will now show by structural induction that all these subformulas (and, hence, also \(\phi\)) have two semantic properties, which we call the monotonicity property and the small witness property (with respect to the \(C_{i}\)). Afterwards, we will show that these two properties allow us to apply the color coding technique. Establishing the monotonicity and small witness properties. Some notations will be useful: Given a \(\tau\)-structure \(\mathcal{A}\) with universe \(A\) and given sets \(A_{i}\subseteq A\) for \(i\in\{1,\ldots,k\}\), let us write \(\mathcal{A}\models\phi(A_{1},\ldots,A_{k})\) to indicate that \(\mathcal{B}\) is a model of \(\phi\) where \(\mathcal{B}\) is the \(\tau_{k\text{-colors}}\)-structure with universe \(A\) in which all symbols from \(\tau\) are interpreted as in \(\mathcal{A}\) and in which the symbol \(C_{i}\) is interpreted as \(A_{i}\), that is, \(C_{i}^{\mathcal{B}}=A_{i}\). Subformulas \(\gamma\) of \(\phi\) may have free variables and suppose that \(x_{1}\) to \(x_{m}\) are the free variables in \(\gamma\) and let \(a_{i}\in A\) for \(i\in\{1,\ldots,m\}\). We write \(\mathcal{A}\models\gamma(A_{1},\ldots,A_{k},a_{1},\ldots,a_{m})\) to indicate that \(\gamma\) holds in the just-described structure \(\mathcal{B}\) when each \(x_{i}\) is interpreted as \(a_{i}\). **Definition 2**. : _Let \(\gamma\) be a \(\eta_{\text{-colors}}\)-formula with free variables \(x_{1}\) to \(x_{m}\).