= Existential second-order logic
{title2=$\exists\mathrm{SO}$}
An <existential second-order logic> sentence has the form
$$
\exists R_1\cdots\exists R_m\,\varphi,
$$
where each $R_i$ is a <second-order relation variable> of fixed finite arity $k_i$ and $\varphi$ 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 $\varphi$.
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.
Back to article page
