= Second-order encoding of three-colorability
{title2=$\Phi_3$}
Represent a finite <simple graph> by a domain $D$ of <vertices> and a symmetric, irreflexive <binary relation> $E$ for <graph adjacency>. Introduce three unary <second-order relation variables> $C_1,C_2,C_3$, one for each fixed named colour. Define the following abbreviations for <first-order formulas> in this expanded <first-order signature>:
$$
\begin{aligned}
\operatorname{One}(x)&:=(C_1(x)\lor C_2(x)\lor C_3(x))\\
&\quad\land\neg(C_1(x)\land C_2(x))\\
&\quad\land\neg(C_1(x)\land C_3(x))\\
&\quad\land\neg(C_2(x)\land C_3(x)),\\
\operatorname{Different}(x,y)&:=\neg(C_1(x)\land C_1(y))\\
&\quad\land\neg(C_2(x)\land C_2(y))\\
&\quad\land\neg(C_3(x)\land C_3(y)).
\end{aligned}
$$
Then the <existential second-order logic> sentence
$$
\Phi_3:=\exists C_1\exists C_2\exists C_3\,
\bigl(\forall x\,\operatorname{One}(x)\ \land\ \forall x\forall y\,(E(x,y)\to\operatorname{Different}(x,y))\bigr)
$$
asserts that every <vertex> receives exactly one of the three colours and adjacent <vertices> receive different colours. The first clause gives coverage and pairwise disjointness of the three <subsets>; the second makes each <subset> an <independent set>. Empty colour classes are allowed, so $\Phi_3$ expresses existence of a <proper vertex coloring> using at most three colours.
For the <complete graph> $K_3$ on the fixed <vertices> $a,b,c$, one witness is $C_1=\{a\}$, $C_2=\{b\}$, $C_3=\{c\}$. Each <vertex> satisfies exactly one predicate, and each of the three <edges> joins different predicates. Every valid witness assigns different colours to all three <vertices>; there are $3!=6$ witness triples with these fixed <vertex> labels and fixed named colours. We are counting assignments, without identifying them under colour permutations or <graph isomorphisms>. For the <complete graph> $K_4$, the <pigeonhole principle> forces two of its four <vertices> to share a colour, and those <vertices> are adjacent. Thus it has no witness triple. This calculation illustrates a <complexity certificate> without requiring the reader to reconstruct a machine computation.
\Image[/second-order-coloring-witness.png]
{title=Six relation witnesses for the labeled complete graph K3, and why K4 has none}
Reproduce the diagram by running `python ../second-order-coloring-witness.py` from the repository's `_media` directory. The script checks all witness triples for these two <complete graphs> before drawing them.
Back to article page
