MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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?

share|cite|improve this question
What prevents a trivial solution: if $S$ is a valid sentence, then take $S'$ to be $\forall x\ x=x$, and if not, then take $S'$ to be an invalid sentence in your desired form. – Joel David Hamkins Nov 1 '12 at 0:10
up vote 3 down vote accepted

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}$.

share|cite|improve this answer
It’s good to see the site back on. I actually wrote up this answer two days ago, but the server went dead before I managed to upload it. – Emil Jeřábek Nov 1 '12 at 11:38

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.