Fagin's theorem

Remarks

From 2 to 1: a machine guesses the relations $R_1, \ldots, R_k$ on the finite universe, which takes polynomially many bits. It then checks the first-order sentence $\varphi$, which takes polynomial time for a fixed $\varphi$. From 1 to 2: the sentence guesses a linear order of the universe and relations that encode an accepting computation of the machine. The computation of length $n^c$ is coded with tuples of length $c$, and $\varphi$ checks that each step follows the transition rules.

Example: the class of finite graphs that admit a proper colouring with three colours is in NP. It is defined by the sentence $\exists R \, \exists G \, \exists B \, \varphi$. Here $\varphi$ says that each vertex lies in $R$, $G$ or $B$, and that no edge joins two vertices in the same set.

Going deeper

For a student

Fagin's theorem started descriptive complexity, which characterises complexity classes by logics without any reference to machines. It shows that NP is closed under complement if and only if existential second-order logic has the same power as universal second-order logic on finite structures. Other results of this kind characterise P on ordered finite structures by first-order logic with a least fixed point operator. The theorem belongs to finite model theory, where classical tools such as compactness are not available.