 Full semantics for second-order logic

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.