# On the Descriptive Complexity of Color Coding +
## 3 Syntactic Properties Allowing Color Coding
### Formulas with Weak Quantifiers
Finally, it will also be useful to assume that the formula has been \"flattened\" as in the proof Theorem 1 (one can loosely think of this as bringing the formula \"locally into disjunctive normal form\"): We use the distributive laws of propositional logic to repeatedly replace subformulas of the form \((\alpha\vee\beta)\wedge\gamma\) by \((\alpha\wedge\gamma)\vee(\beta\wedge\gamma)\) and \(\alpha\wedge(\beta\vee\gamma)\) by \((\alpha\wedge\beta)\vee(\alpha\wedge\gamma)\). Note that this transformation does not change which variables are weak. For our running example, applying the described preprocessing yields:  
\[\phi\equiv\forall v\exists a\big{(}\exists\dot{x}_{1}(Ea\dot{x}_{1}\wedge\exists \dot{x}_{2}(\dot{x}_{2}\
eq\dot{x}_{1}))\wedge\forall c\exists\dot{x}_{3} \exists\dot{x}_{4}(E\dot{x}_{3}\dot{x}_{4}\vee\exists z(\dot{x}_{3}\
eq\dot{x}_ {4}\wedge Pz\wedge Qcaz))\big{)}.\]  
Syntactic transformations I: blocks of weak quantifiers. The first interesting transformation is the following: We wish to move weak quantifiers \"as far up the syntax tree as possible.\" To achieve this, we apply the following equivalences as long as possible by always replacing the left-hand side (and also commutatively equivalent formulas) by the right-hand side:  
\[\exists\dot{x}(\alpha)\wedge\beta \equiv\exists\dot{x}(\alpha\wedge\beta),\] \[\exists\dot{x}(\alpha)\vee\beta \equiv\exists\dot{x}(\alpha\vee\beta),\] \[\exists y\exists\dot{x}(\alpha) \equiv\exists x\exists y(\alpha).\]  
Note that \(\beta\) does not contain \(\dot{x}\) since we made all weak variables distinct and, of course, by \(\exists y\) we mean a strong quantifier. Once the transformations have been applied exhaustively, all weak quantifiers will be directly preceded in \(\phi\) by either a universal quantifier or another weak quantifier. This means that all weak quantifiers are now arranged in blocks inside \(\phi\), each block being preceded by a universal quantifier. \[\phi\equiv\forall v\exists\dot{x}_{1}\exists\dot{x}_{2}\exists a\big{(}Ea\dot{ x}_{1}\wedge\dot{x}_{2}\
eq\dot{x}_{1}\wedge\forall c\exists\dot{x}_{3} \exists\dot{x}_{4}(E\dot{x}_{3}\dot{x}_{4}\vee\exists z(\dot{x}_{3}\
eq\dot{x}_ {4}\wedge Pz\wedge Qcaz))\big{)}\]  
Syntactic transformations II: weak and strong literals. In order to apply color coding later on, it will be useful to have only three kinds of literals in \(\phi\):  
1. Strong literals are literals that do not contain any weak variables. 2. Weak equalities are literals of the form \(\dot{x}=y\) involving exactly one strong variable that is existentially bound inside the weak variable's scope: \[\exists\dot{x}(\ldots\exists y(\ldots\dot{x}=y\ldots)\ldots).\]
3. Weak inequalities are literals of the form \(\dot{x}\
eq\dot{y}\) for two weak variables. Let us call all other kinds of literals bad. This includes literals like \(E\dot{x}\dot{x}\) or \(Ez\dot{y}\), contain a relation symbol and some weak variables, but also inequalities \(\dot{x}\
eq y\) involving a weak and a strong variable, equalities \(\dot{x}=\dot{y}\) involving two weak variables, or an equality literal like the one in \(\forall y\exists\dot{x}(\dot{x}=y)\). Finally, literals involving the successor function and weak variables are also bad. In order to get rid of the bad literals, we will replace them by equivalent formulas that do not contain any bad literals. The idea is that we bind the variable or term that we wish to get rid of using a new existential quantifier. In order to avoid introducing too many new variables, for all of the following transformations we use the set of fresh variables \(v_{1}\), \(v_{2}\), and so on, where we may need more than one of these variables per literal, but will need no more than \(O(\operatorname{arity}(\tau))\) (recall that \(\operatorname{arity}(\tau)\) is the maximum arity of relation symbols in \(\tau\)). Let \(\lambda\) be a bad literal, that is, let it contain a weak variable \(\dot{x}\), but neither be a weak equality nor a weak inequality.