Fagin's theorem

Fix a finite relational first-order signature $\tau$, and let $\mathcal{K}$ be a class of finite nonempty $\tau$-first-order structures closed under isomorphism. Fagin's theorem states that $\mathcal{K}$ is definable by one existential second-order logic sentence under full semantics for second-order logic if and only if its language of standard finite encodings belongs to NP. A standard encoding numbers the domain $\{0,\dots ,n-1\}$ and lists membership bits for each input relation, together with $n$; take an explicit encoding whose length is at least $n$. The encoding language contains all numbered copies of members of $\mathcal{K}$, with malformed encodings rejected. The isomorphism condition makes membership a property of the structure rather than an arbitrary choice of labels. Changing between the usual explicit encodings preserves the NP characterization by polynomial time translations.

The forward direction is the witness-and-verifier calculation in existential second-order logic. For the reverse direction, the guiding idea is to encode an accepting nondeterministic computation using second-order relation variables: fixed-length tuples of domain elements index enough time steps and storage positions for a polynomial time computation. A first-order sentence checks the initial input, legal transitions, and acceptance. The number of tuples grows with the input, although the checking sentence stays fixed. No total order must be supplied as part of the input first-order signature: an auxiliary total order can itself be existentially guessed and constrained by a first-order sentence. Isomorphism invariance ensures that a change of this auxiliary numbering does not change membership in $\mathcal{K}$.

The second-order encoding of three-colorability is a small instance of the forward direction. The beauty of Fagin's theorem is the complete correspondence: the computational class NP can be characterized by the shape of a logical description, without mentioning a particular machine in the statement. The scope is finite relational first-order structures and fixed sentences; it is not a claim about deciding arbitrary second-order logic sentences or about arbitrary infinite domains.

Ronald Fagin published the result in Generalized First-Order Spectra and Polynomial-Time Recognizable Sets, SIAM-AMS Proceedings 7 (1974), pp. 43–73, Section 4. The original paper frames the correspondence using classes of finite expansions and their encodings. Fagin's author-maintained publication list explains that the abstract in the available copy was added in 2019; its modern summary should therefore not be mistaken for part of the 1974 printing.