# On the Descriptive Complexity of Color Coding +
## 3 Syntactic Properties Allowing Color Coding
### Formulas with Weak Quantifiers
_There is an_ \(l\)_-coloring_ \(\mathcal{B}\) _of_ \(\mathcal{A}\) _such that_ \(\mathcal{B}\models\alpha^{\prime}\)_._  
Proof. : For the proof of the claim, it will be useful to apply some syntactic transformations to \(\alpha\) and \(\alpha^{\prime}\). Just like the many transformations we encountered earlier, these transformations yield equivalent formulas and, thus, it suffices to prove the claim for them (since the claim is about the models of \(\alpha\) and \(\alpha^{\prime}\)). However, these transformations are needed only to prove the claim, they are not part of the \"chain of transformations\" that is applied to the original formula (they increase the number of strong variables far too much). In \(\alpha\) there will be some occurrences of literals of the form \(\dot{x}_{i}=y\). For each such occurrence, there will be exactly one subformula in \(\alpha\) of the form \(\exists y(\gamma)\) where \(\gamma\) contains \(\dot{x}_{i}=y\). We now apply two syntactic transformations: First, we replace \(y\) in \(\exists y(\gamma)\) by a fresh new variable \(y_{i}\) (that is, we replace all free occurrences of \(y\) inside \(\gamma\) by \(y_{i}\) and we replace the leading \(\exists y\) by \(\exists y_{i}\)). Second, we \"move all \(\exists y_{i}\) to the front\" by simply deleting all occurrences of \(\exists y_{i}\) from \(\alpha\), resulting in a formula \(\delta\), and then adding the block \(\exists y_{1}\cdots\exists y_{k}\) before \(\delta\). As an example, if we apply these transformations to \(\alpha=\exists v_{1}(\dot{x}_{7}=v_{1}\wedge\exists v_{2}(\dot{x}_{8}=v_{2} \wedge Ev_{1}v_{2}))\), the first transformation yields  
\[\exists\dot{x}(\alpha)\vee\beta \equiv\exists\dot{x}(\alpha\vee\beta),\]0  
and the second one yield the new  
\[\exists\dot{x}(\alpha)\vee\beta \equiv\exists\dot{x}(\alpha\vee\beta),\]1  
In \(\alpha^{\prime}\), we apply exactly the same transformations, only now the literals we look for are not \(\dot{x}_{i}=y\), but \(C_{y}y\). We still apply the same renaming of \(y\) (namely to \(y_{i}\) and not to \(y_{j}\)) as in \(\alpha\) and apply the same movement of the quantifiers. This results in a new formula \(\alpha^{\prime}\) of the form \(\exists y_{1}\cdots\exists y_{k}(\delta^{\prime})\). For \(\alpha^{\prime}=\exists v_{1}(C_{1}v_{1}\wedge\exists v_{2}(C_{2}v_{2}\wedge Ev _{1}v_{2}))\) we get the new  
\[\exists\dot{x}(\alpha)\vee\beta \equiv\exists\dot{x}(\alpha\vee\beta),\]2  
and \(\delta^{\prime}\) is now the inner part without the quantifiers. Let us now prove the claim. The first two items are trivially equivalent by the definition of \(\text{distinct}(P_{1},\ldots,P_{l})\). The second statement implies the third: To show this, for \(j\in\{1,\ldots,l\}\) we first set \(C_{j}^{\mathcal{B}}=\{a_{i}\mid\dot{x}_{i}\in P_{j}\}\) and then add \(|\mathcal{A}|\setminus\{a_{1},\ldots,a_{k}\}\) to, say, \(C_{1}^{\mathcal{B}}\) in order to create a correct partition. This setting clearly ensures that whenever \(\dot{x}_{i}=y\) holds in \(\alpha\), we also have \(C_{j}y\) holding in \(\alpha^{\prime}\). Since \(\alpha^{\prime}\) differs from \(\alpha\) only on the literals of the form \(\dot{x}_{i}=y\) (which got replaced by \(C_{j}y\)), since we just saw that when \(\dot{x}_{i}=y\) holds in \(\alpha\), the replacements \(C_{j}y\) holds in \(\alpha^{\prime}\), and since \(\alpha\) has the monotonicity property (by which it does matter when more literals of the form \(C_{j}y\) hold in \(\alpha^{\prime}\) than did in \(\alpha\)), we get the third statement. The third statement implies the second: Let an \(l\)-coloring \(\mathcal{B}\) of \(\mathcal{A}\) be given with \(\mathcal{B}\models\alpha^{\prime}\). Since \(\alpha^{\prime}=\exists y_{1}\cdots\exists y_{k}(\delta^{\prime})\), there must now be elements \(b_{1},\ldots,b_{k}\in|\mathcal{A}|\) such that \(\mathcal{B}\models\delta^{\prime}(b_{1},\ldots,b_{k})\). We define new elements \(a_{i}\in|\mathcal{A}|\) as follows: If \(b_{i}\in C_{l}^{\mathcal{B}}\), let \(a_{i}=b_{i}\).