Fagin's theorem

For example, consider the problem of deciding if a graph is 3-colorable. This is NP-complete. By Fagin’s theorem, there is a second order existential formula ${\displaystyle \phi }$, such that a graph is 3-colorable if and only if the graph, as a finite model for ${\displaystyle \phi }$, semantically implies ${\displaystyle \phi }$. Explicitly, here is one such formula:^[4]

(∃A, B, C)(∀v)[(A(v) ∨ B(v) ∨ C(v)) ∧ (∀w)(E(v, w) → ¬(A(v) ∧ A(w)) ∧ ¬(B(v) ∧ B(w)) ∧ ¬(C(v) ∧ C(w)))]

In this formula, A, B, or C are to be interpreted as the sets of vertices colored with the 3 colors, and E(v, w) is to be interpreted as saying the vertices v, w share an edge. The formula then states that no two adjacent vertices have the same color.

Note that there is no need to explicitly enforce each vertex to have exactly 1 color, just at least 1 color. Since, if we allow more than 1 color per vertex, and no two adjacent vertices have the same color, then we certainly can have each vertex to have exactly 1 color, and still no two adjacent vertices have the same color.

The 1999 textbook by Immerman provides a detailed proof of the theorem. A sketch is given here.^[5]

It is straightforward to show that every existential second-order formula can be recognized in NP, by nondeterministically choosing the value of all existentially-qualified variables, so the main part of the proof is to show that every language in NP can be described by an existential second-order formula. To do so, one can use second-order existential quantifiers to arbitrarily choose a computation tableau. In more detail, for every timestep of an execution trace of a non-deterministic Turing machine, this tableau encodes the state of the Turing machine, its position in the tape, the contents of every tape cell, and which nondeterministic choice the machine makes at that step. A first-order formula can constrain this encoded information so that it describes a valid execution trace, one in which the tape contents and Turing machine state and position at each timestep follow from the previous timestep.

A key lemma used in the proof is that it is possible to encode a linear order of length ${\displaystyle n^{k}}$ (such as the linear orders of timesteps and tape contents at any timestep) as a ${\displaystyle 2k}$-ary relation ${\displaystyle R}$ on a universe ${\displaystyle A}$ of size ${\displaystyle n}$. One way to achieve this is to choose a linear ordering ${\displaystyle L}$ of ${\displaystyle A}$ and then define ${\displaystyle R}$ to be the lexicographical ordering of ${\displaystyle k}$-tuples from ${\displaystyle A}$ with respect to ${\displaystyle L}$.

• Spectrum of a sentence