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.

Under full semantics for second-order logic, a second-order relation variable of arity $k$ ranges over exactly $\mathcal{P}(D^k)$, the external power set of the appropriate Cartesian product. Thusand universal quantification over $R$ checks every such subset. Here the power set is taken in the ambient mathematical universe, not merely among relations definable by formulas or represented by objects inside $D$.

For $D=\{a,b,c\}$, a unary second-order relation variable has eight possible values, including the three singletons needed by the second-order encoding of three-colorability. The three unary witnesses can range independently over those eight subsets, giving $8^3=512$ candidate triples before the first-order sentence is checked; only six triples pass for the complete graph $K_3$. For $K_4$, there are $16^3=4096$ candidate triples and none passes. Distinguishing the range of candidates from the constraints on valid witnesses clarifies both full semantics for second-order logic and the verifier view of NP.

The appeal of full semantics for second-order logic is its literal reading of assertions about every subset or every relation. A first-order structure fixes the second-order ranges automatically, in contrast to Henkin semantics. That expressive force comes with a limitation: there is no effective, sound deductive system complete for all valid second-order logic sentences under full semantics for second-order logic. This limitation and the change of intended models motivating Henkin semantics are described at the start of ^[ref].

For a domain $V_{\lambda }$, an external functional graph with all its individual ordered pairs in $V_{\lambda }$ is therefore available, even if the whole graph does not belong to $V_{\lambda }$. More generally, a binary second-order relation variable can denote any external subset of $V_{\lambda }\times V_{\lambda }$; its ordered pairs need not themselves be elements of the individual domain. Having endpoints in the domain is what matters. This distinction between internal objects and externally available relations is essential when applying second-order logic to the cumulative hierarchy.

In Henkin semantics, a domain $D$ is accompanied by designated ranges ${\mathcal{H}}_k\subseteq \mathcal{P}(D^k)$ for second-order relation variables of each arity $k$. A formula $\exists R\phi (R)$ searches only ${\mathcal{H}}_k$, and $\forall R\phi (R)$ checks only ${\mathcal{H}}_k$. These ranges can be proper subcollections of the external power set. Keeping $D$ and its input relations fixed therefore need not fix the truth of a second-order logic sentence.

As a toy illustration of restricted quantification, take $D=\{a,b\}$ and unary range ${\mathcal{H}}_1=\{\varnothing ,D\}$. The sentenceis true under full semantics for second-order logic, but false with this selected range, because neither singleton is available. Likewise, on the complete graph $K_3$, the unary range $\{\varnothing ,D\}$ admits no witness for the second-order encoding of three-colorability, even though a usual proper vertex coloring exists. This toy range illustrates the truth definition only: it fails second-order comprehension for the formula $x=a$, and is not a model of a system requiring that comprehension instance.

Admissible Henkin semantics for a specified deductive system must satisfy its axioms, including its chosen second-order comprehension requirements or analogous closure conditions for predicate abstraction. Closure is relative to the permitted formulas and parameters, rather than a blanket property of every selected family. In particular, on a finite domain, allowing logical equality, individual parameters, all finite logical disjunctions, and comprehension for those formulas forces every finite-arity relation to be available: enumerate its tuples and disjoin the formulas naming them. Thus a proper restricted finite range cannot satisfy that entire scheme.

Treating each ${\mathcal{H}}_k$ as an additional sort, with an application relation between its members and $k$ individuals, translates this relational presentation into first-order logic with several sorts. Include axioms saying that predicates with the same members are equal, together with whatever second-order comprehension the system requires. This makes Henkin semantics useful for bringing first-order logic methods to reasoning about predicates; it does not license conclusions about all external relations.

Leon Henkin's Completeness in the Theory of Types, Journal of Symbolic Logic 15 (1950), pp. 81–91 develops general models and proves completeness for his typed deductive system. Its opening footnote 5 explicitly discusses closure under operations associated with formula formation. Henkin later described the discovery process in his ^[ref]; that later account is a historical recollection, distinct from the original publication.

Second-order logic extends first-order logic by allowing existential quantification and universal quantification over second-order relation variables, as well as over individual objects. In the relational presentation used here, an individual variable $x$ ranges over a domain $D$, while a second-order relation variable $R$ of arity $k$ denotes a subset of $D^k$. Unary second-order relation variables denote subsets of $D$; binary ones denote binary relations. Presentations with function variables can instead describe their graphs by second-order relation variables, with first-order formulas requiring a unique output for every input.

For a graph with vertices $D$ and fixed graph adjacency $E$, the first-order sentence $\forall x\exists yE(x,y)$ says that every vertex has a neighbour. It selects individual vertices while $E$ retains its given interpretation. By contrast,selects an entire subset $P$ and says that it is a nonempty independent set. Here $P$ is a unary second-order relation variable, rather than a symbol in the input first-order signature. This particular property also has a simple first-order sentence on simple graphs; the example illustrates the change in what can be selected, rather than proving a separation in expressive power.

The usefulness of second-order logic is that one can describe a whole proposed solution, such as a graph coloring, and then impose local constraints on it. Syntax alone does not specify which proposed relations are available: full semantics for second-order logic permits all external subsets of $D^k$, whereas Henkin semantics supplies designated ranges. The second-order encoding of three-colorability makes this distinction concrete.