  Color coding is an algorithmic technique used in parameterized complexity
theory to detect "small" structures inside graphs. The idea is to derandomize
algorithms that first randomly color a graph and then search for an
easily-detectable, small color pattern. We transfer color coding to the world
of descriptive complexity theory by characterizing -- purely in terms of the
syntactic structure of describing formulas -- when the powerful second-order
quantifiers representing a random coloring can be replaced by equivalent,
simple first-order formulas. Building on this result, we identify syntactic
properties of first-order quantifiers that can be eliminated from formulas
describing parameterized problems. The result applies to many packing and
embedding problems, but also to the long path problem. Together with a new
result on the parameterized complexity of formula families involving only a
fixed number of variables, we get that many problems lie in FPT just because of
the way they are commonly described using logical formulas.
