= Fagin's theorem
{c}
{wiki}
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,\ldots,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 https://s3.us.cloud-object-storage.appdomain.cloud/res-files/500-genspec.pdf[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 https://ronfagin.com/papers/[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.
Back to article page
