Fagin's Theorem: NP and Existential Second-Order Logic

One of the most beautiful results in descriptive complexity is Fagin’s theorem, which gives a purely logical characterization of the complexity class $\mathrm{NP}$. No machines, no resources, no clocks — just logic.

Setup

We work over finite relational structures. A vocabulary $\tau$ is a finite set of relation symbols, each with an associated arity. A $\tau$-structure $\mathfrak{A}$ consists of a finite universe $A$ together with an interpretation of each symbol in $\tau$.

Existential second-order logic ($\Sigma_1^1$) allows existential quantification over relations:

$$ \varphi \;=\; \exists R_1 \cdots \exists R_k \; \psi $$

where $\psi$ is a first-order formula over the enriched vocabulary $\tau \cup \{R_1, \ldots, R_k\}$.

The Theorem

Theorem (Fagin, 1974). A class of finite structures is in $\mathrm{NP}$ if and only if it is definable by a sentence of existential second-order logic ($\Sigma_1^1$).

Proof. $(\Rightarrow)$: Given an NP machine $M$ accepting instances of size $n$ in time $n^k$, we write a $\Sigma_1^1$ sentence that guesses the computation tableau of $M$ as a relation of arity $3k$ and verifies the tableau axioms in first-order logic. $(\Leftarrow)$: Given $\varphi = \exists \vec{R}\, \psi \in \Sigma_1^1$, the NP machine nondeterministically guesses an assignment to $\vec{R}$ (polynomial in the structure size) and checks $\psi$ in polynomial time. ∎

Why This Matters

The theorem isolates the combinatorial essence of nondeterminism: it is exactly the ability to guess a witness relation. The proof is constructive in both directions, and the translation is tight.

Remark. Fagin's proof predates the PCP theorem, the polynomial hierarchy, and most of modern complexity theory. It remains one of the cleanest "machine-free" characterizations of a natural complexity class.

A Corollary

Corollary. Graph 3-colorability is $\Sigma_1^1$-definable. Concretely: $$ \exists C \;\Big[\, \forall x\, \bigvee_{i=1}^{3} C_i(x) \;\wedge\; \forall x\, \bigwedge_{i \neq j} \neg(C_i(x) \wedge C_j(x)) \;\wedge\; \forall x\forall y\, E(x,y) \to \bigwedge_i \neg(C_i(x) \wedge C_i(y)) \Big] $$

And that is why, at least in the finite, $\mathrm{NP}$ is not just a class of hard problems — it is a language about witnesses.