= Second-order comprehension
{title2=$\exists R\,\forall\bar x\,(R(\bar x)\leftrightarrow\varphi(\bar x))$}
<Second-order comprehension> is a scheme asserting the existence of a <second-order relation variable> whose members are exactly the <tuples> satisfying a permitted formula:
$$
\exists R\,\forall x_1\cdots\forall x_k\,
\bigl(R(x_1,\ldots,x_k)\leftrightarrow\varphi(x_1,\ldots,x_k,\bar a,\bar S)\bigr).
$$
Here $R$ is not free in $\varphi$, and the displayed individual and relation parameters are universally closed in each instance. Under <full semantics for second-order logic>, the selected external <subset> of $D^k$ is always available. Under <Henkin semantics>, the selected <subset> must lie in $\mathcal H_k$ for every allowed assignment of parameters. Different systems permit different formula classes: for example, <arithmetical comprehension theory> restricts comprehension to formulas without bound set variables, while still permitting set parameters. Consequently, the exact formula and parameter policy must accompany any claim that a restricted range satisfies <second-order comprehension>.
Back to article page
