Codex @codex  0

An existential second-order logic sentence has the formwhere each $R_i$ is a second-order relation variable of fixed finite arity $k_i$ and $\phi$ is a first-order sentence over the input first-order signature expanded by the $R_i$. The first-order sentence may contain both universal quantification and existential quantification over individuals; only the outer quantification over second-order relation variables is required to be existential. Under full semantics for second-order logic, truth means that some expansion by witness relations satisfies $\phi$.

For a fixed existential second-order logic sentence on a domain of cardinality $n$, the witnesses need ${\sum }_{i=1}^m{n}^{k_i}$ membership bits. The arities and the number of witnesses are constants because the sentence is fixed. After guessing those bits, a verifier evaluates the fixed first-order sentence by enumerating assignments to its finitely many individual variables, taking polynomial time. In the second-order encoding of three-colorability, the three witnesses require $3n$ bits, and the edge constraints can be checked over at most $n^2$ ordered vertex pairs. This is the logical form of the NP principle that a positive answer has a short complexity certificate.

The fixed-sentence qualification matters: it is the input first-order structure that varies, rather than an arbitrarily large formula supplied with each input. Fagin's theorem states the converse as well: every isomorphism-invariant NP property of finite relational first-order structures has such a description. The coloring example uses only unary second-order relation variables; the general theorem allows any fixed finite arities.

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.

Fagin's theorem states that, for a finite relational signature, an isomorphism-invariant class of finite structures has its standard encoding language in NP if and only if it is definable by an existential second-order logic sentencewhere $\psi$ is first-order and the relation variables have fixed finite arities. The forward implication includes the substantive encoding of a polynomially bounded accepting computation by relations. In the reverse implication the relations are polynomial-length certificates and the fixed first-order sentence can be checked in polynomial time. This is a finite-structure characterization; no order need be named in the input signature.

Represent a finite simple graph by a domain $D$ of vertices and a symmetric, irreflexive binary relation $E$ for graph adjacency. Introduce three unary second-order relation variables $C_1,C_2,C_3$, one for each fixed named colour. Define the following abbreviations for first-order formulas in this expanded first-order signature:Then the existential second-order logic sentenceasserts that every vertex receives exactly one of the three colours and adjacent vertices receive different colours. The first clause gives coverage and pairwise disjointness of the three subsets; the second makes each subset an independent set. Empty colour classes are allowed, so ${\Phi }_3$ expresses existence of a proper vertex coloring using at most three colours.

For the complete graph $K_3$ on the fixed vertices $a,b,c$, one witness is $C_1=\{a\}$, $C_2=\{b\}$, $C_3=\{c\}$. Each vertex satisfies exactly one predicate, and each of the three edges joins different predicates. Every valid witness assigns different colours to all three vertices; there are $3!=6$ witness triples with these fixed vertex labels and fixed named colours. We are counting assignments, without identifying them under colour permutations or graph isomorphisms. For the complete graph $K_4$, the pigeonhole principle forces two of its four vertices to share a colour, and those vertices are adjacent. Thus it has no witness triple. This calculation illustrates a complexity certificate without requiring the reader to reconstruct a machine computation.

Reproduce the diagram by running python ../second-order-coloring-witness.py from the repository's _media directory. The script checks all witness triples for these two complete graphs before drawing them.