Fagin's theorem
Existential second order logic captures NP
- 2 min read
- 2 chapters
Explore on Lably
ToursExplore Lably’s 3D toursIt was proven by Ronald Fagin in 1973 in his doctoral thesis, and appears in his 1974 paper. The arity required by the second-order formula was improved (in one direction) by James Lynch in 1981, and several results of Étienne Grandjean have provided tighter bounds on nondeterministic random-access machines.
Example
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 , such that a graph is 3-colorable if and only if the graph, as a finite model for , semantically implies . Explicitly, here is one such formula:
(∃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.
Sign in to keep reading
One more chapter is free with a Lably account.
Proof
The 1999 textbook by Immerman provides a detailed proof of the theorem. A sketch is given here.
In one direction, given an existential second-order formula, and a purported model, the model can be checked in NP, by nondeterministically choosing the value of all existentially-quantified variables
In the other direction, given a language in NP, we describe it 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. Then, we write down a first-order formula, so that a tableau is a valid execution trace iff it satisfies the formula. Next, we perform an existential quantification over all possible tableaus of the given size.
A key lemma used in the proof is that it is possible to encode a linear order of length (such as the linear orders of timesteps and tape contents at any timestep) as a -ary relation on a universe of size . One way to achieve this is to choose a linear ordering of and then define to be the lexicographical ordering of -tuples from with respect to .