= 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>. Thus
$$
\exists R\,\varphi(R)\quad\text{means}\quad
\text{some }S\subseteq D^k\text{ satisfies }\varphi(S),
$$
and <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 https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/completeness-in-the-theory-of-types1/551D2896D3C6F197030D3D8EEA911F1E[Henkin's 1950 paper]{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>.
Back to article page
