= Second-order logic
{title2=$\mathrm{SO}$}
{wiki}
<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 y\,E(x,y)$ says that every <vertex> has a neighbour. It selects individual <vertices> while $E$ retains its given interpretation. By contrast,
$$
\exists P\,\bigl(\exists x\,P(x)\ \land\ \forall x\forall y\,((P(x)\land P(y))\to\neg E(x,y))\bigr)
$$
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.
Back to article page
