Normal form in second-order logic

Question

In a first-order logic, L, it is possible to transform a sentence, S, containing variables into a sentence S' in so-called 'clause form' - i.e. with a matrix in conjunctive normal form and a prefix consisting of only universal quantifiers - such that S is valid iff S' is. If L is expanded to a second-order language containing variables and quantifiers ranging over first-order predicates, but with no higher-order predicates (i.e. none that take first-order predicates as their arguments) is it still the case that sentences of the expanded language can always be put into clause form in a way that preserves validity?

Answer 1

First, if you don’t place any restrictions on the transformation, you can actually make $S'$ as simple as you want in any logic: if $S$ is valid, let $S'$ be any fixed tautology, otherwise let $S'$ be a fixed non-tautology. In order to rule out such a trivial answer, I will henceforth assume that the transformation $S\mapsto S'$ is required to be computable.

Second, it’s stated wrongly in the question. In first-order logic, you can introduce Skolem functions to make any sentence universal, but this transformation does not preserve validity, it preserves satisfiability. If you want to make $S'$ valid iff $S$ is, you need the dual transformation: introduce Herbrand functions to make the sentence existential.

In second-order logic, preserving validity, you can transform any sentence into a block of existential second-order quantifiers, followed by a block of first-order universal quantifiers, followed by an open matrix (say, in CNF). I’ll write this as $\exists^{SO}\forall^{FO}$. This relies on having second-order function variables; if you only allow second-order predicate variables, you need $\exists ^{SO}\forall^{FO}\exists^{FO}$. Dually, while preserving satisfiability, you can make any sentence $\forall^{SO}\exists^{FO}$ using function variables, or $\forall^{SO}\exists^{FO}\forall^{FO}$ using predicate variables.

The basic idea is as follows (I will state it for satisfiability, as it is more intuitive that way). Second-order quantification over a model $M$ can be simulated by first-order quantification over something like $(M,\mathcal P(M))$. So, introduce predicates $M,P,E$, and include in $S'$ the sentence

$$\tag{$*$}\forall X\,\exists u\,(P(u)\land\forall x\,(M(x)\to(x\in X\leftrightarrow E(x,u)))).$$

Elements satisfying $M(x)$ will represent elements of the original model $M$, and elements satisfying $P(u)$ will represents all subsets of $M$. Similarly, you can introduce predicates and axioms similar to $(*)$ simulating $\mathcal P(M^n )$ whenever an $n$-ary predicate variable appears in $S$, and similarly for function variables. Then you can rewrite $S$ as a first-order formula quantifying over elements satisfying these extra predicates instead of second-order quantification.

The crucial thing is that $(*)$ has only universal second-order quantifiers followed by a first-order formula, so in this way, you can transform any sentence into $\forall^{SO}\exists^{FO}\forall^{FO}\cdots \exists^{FO}\forall^{FO}$. Using Herbrand functions, any first-order formula is equivalent to a $\forall^{SO}\exists^{FO}$ formula, where the second-order quantifiers quantify over the Herbrand functions. This makes $S'$ into $\forall^{SO}\exists^{FO}$. The second-order function variables introduced in the last step can be replaced by predicate variables ranging over their graphs if necessary, but then you need extra first-order quantifiers to express that these predicates are really graphs of functions and to extract their value; it is possible to do this within $\forall^{SO}\exists^{FO}\forall^{FO}$.