# On the Descriptive Complexity of Color Coding +
## 3 Syntactic Properties Allowing Color Coding
### Formulas with Weak Quantifiers
Thus, the requirement \"in any subformula of \(\psi_{i}\) of the form \(\alpha\wedge\beta\) only \(\alpha\) or \(\beta\)--but not both--may use \(\dot{x}\) in a literal that is not a weak inequality\" from the definition of weak variables just boils down to \"\(\dot{x}\) may only be used once in \(\psi_{i}\) in a literal that is not a weak inequality.\" Since weak variables cannot be present in strong literals, this means, in particular, that \(\dot{x}\) is now only used in (at most) a single weak equality \(\dot{x}=y\) and otherwise only in weak inequalities. Syntactic transformations IV: completing weak inequalities. The last step before we can apply the color coding method is to \"complete\" the conjunctions of weak inequalities. After all the previous transformations have been applied, each block of weak quantifiers has now the form \(\exists\dot{x}_{1}\cdots\exists\dot{x}_{k}\big{(}\bigwedge_{j}\lambda_{i} \wedge\alpha\big{)}\) where the \(\lambda_{i}\) are all weak inequalities (between some or all pairs of \(\dot{x}_{1}\) to \(\dot{x}_{k}\)) and \(\alpha\) contains no weak inequalities involving the \(\dot{x}_{i}\) (but may contain one weak equality for each \(\dot{x}_{i}\)). Of course, the weak variables need not be \(\dot{x}_{1}\) to \(\dot{x}_{k}\), but let us assume this to keep to notation simple. The formula \(\bigwedge_{i}\lambda_{i}\) expresses that some of the variables \(\dot{x}_{i}\) must be different. If the formula encompasses all possible weak inequalities between distinct \(\dot{x}_{i}\) and \(\dot{x}_{j}\), then the formula would require that all \(\dot{x}_{i}\) must be distinct--exactly the situation in which color coding can be applied. However, some weak inequalities may be \"missing\" such as in the formula \(\dot{x}_{1}\
eq\dot{x}_{2}\wedge\dot{x}_{2}\
eq\dot{x}_{3}\wedge\dot{x}_{1} \
eq\dot{x}_{3}\wedge\dot{x}_{3}\
eq\dot{x}_{4}\): This formula requires that \(\dot{x}_{1}\) to \(\dot{x}_{3}\) must be distinct and that \(\dot{x}_{4}\) must be different from \(\dot{x}_{3}\)--but it would be allowed that \(\dot{x}_{4}\) equals \(\dot{x}_{1}\) or \(\dot{x}_{2}\). Indeed, it might be the case that the only way to make \(\alpha\) true is to make \(\dot{x}_{1}\) equal to \(\dot{x}_{4}\). This leads to a problem in the context of color coding: We want to color \(\dot{x}_{1}\), \(\dot{x}_{2}\), and \(\dot{x}_{3}\) differently, using, say, red, green, and blue. In order to ensure \(\dot{x}_{3}\
eq\dot{x}_{4}\), we must give \(\dot{x}_{4}\) a color different from blue. However, it would be wrong to color it red or green or using a new color like yellow since each would rule out \(\dot{x}_{4}\) being equal or different from either \(\dot{x}_{1}\) or \(\dot{x}_{2}\)--and each possibility must be considered to ensure that we miss no assignment that makes \(\alpha\) true. The trick at this point is to reduce the problem of missing weak inequalities to the situation where all weak inequalities are present by using a large disjunction over all possible ways to unify weak variables without violating the weak inequalities. In detail, let us call a partition \(P_{1}\dot{\cup}\cdots\dot{\cup}P_{l}\) of the set \(\{\dot{x}_{1},\dots,\dot{x}_{k}\}\) allowed by the \(\lambda_{i}\) if the following holds: For each \(P_{j}\) and any two different \(\dot{x}_{p},\dot{x}_{q}\in P_{j}\) none of the \(\lambda_{i}\) is the inequality \(\dot{x}_{p}\
eq\dot{x}_{q}\). In other words, the \(\lambda_{i}\) do not forbid that the elements of any \(P_{j}\) are identical. Clearly, the partition with \(P_{j}=\{\dot{x}_{j}\}\) is always allowed by any \(\lambda_{i}\), but in the earlier example, the partition \(P_{1}=\{\dot{x}_{1},\dot{x}_{4}\}\), \(P_{2}=\{\dot{x}_{2}\}\), \(P_{3}=\{\dot{x}_{3}\}\) would be allowed, while \(P_{1}=\{\dot{x}_{1}\}\), \(P_{2}=\{\dot{x}_{2}\}\), \(P_{3}=\{\dot{x}_{3},\dot{x}_{4}\}\) would not be.