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

Consider first-order logic with some fixed, relational vocabulary $\tau$. A sentence is a formula in this logic with no free variables.

A sentence is in prenex normal form, if all quantifiers are moved to the front. For example $\exists x\exists y(P(x)\to P(y))$ is in prenex normal form whereas $\exists x( P(x)\lor \exists y(P(x)\to P(y)))$ is not.

Let quantifier rank of a sentence be the maximum number of nested quantifications in it.

Now, we know that quantifier rank is a measure of complexity of a first-order formula in the sense that there are only a finite number of sentences of a fixed quantifier rank up to logical equivalence (lets consider only finite models).

If we have a sentence of the form $\varphi \equiv \exists x(\exists y \alpha(x,y)\lor\exists y \beta(x,y))$, where $\alpha$ and $\beta$ are formulas with two free variables $x$ and $y$, it is straightforward to transform it to a prenex form by simply renaming the occurences of $y$s and shifting quantifiers in front, i.e. $\exists x\exists y_1\exists y_2(\alpha(x,y_1)\lor \beta(x,y_2))$. But now the originating formula had quantifier rank of $2$ when the prenex form formula has quantifier rank $3$.

How would one transform a formula to prenex normal form in a way that would keep the quantifier rank untouched?

share|cite|improve this question
up vote 8 down vote accepted

If you begin with $\psi \equiv (\exists x)R(x) \land (\exists x)(\lnot R(x)) \land (\forall y)S(y)$, the usual prenex form will have depth 3, while the original formula has depth 1. So you are asking how to find an equivalent formula to $\psi$ that only has one quantifier.

Let's assume our language only has two unary relation symbols $R$ and $S$. Then the formula $\psi$ above cannot be equivalent to any one quantifier formula $\phi$. First assume $\phi$ is existential, and true in some model. Then we can make a new model $M$ by adding one more element for which $S$ does not hold. Then $\phi$ is still true in $M$ (it will be preserved under extensions) but $\psi$ is not true in $M$ because $(\forall y)S(y)$ is not true.

Suppose $\phi$ is universal. Take any model with more than 2 elements in which $\psi$ holds, and call one of the elements $c$. Take the submodel $N$ containing just $c$. Then $\phi$ is still true in $N$, because it is preserved under taking substructures, but $\psi$ is not true because $\psi$ requires at least two elements in the domain.

share|cite|improve this answer
Yep, this is it. Thanks for clarifying this up - I somehow took it for granted that such form exists. Silly me... – user10891 May 3 '11 at 13:02

Although Carl has answered the question, I'd like to use it as an excuse to preach about one of my pet peeves, namely the idea that, when defining the Skolem form (or its dual, the Herbrand form) of a sentence, one should first put the sentence into prenex form and then perform the appropriate replacement of certain quantified variables by new function symbols. This is fine for most purely theoretical purposes, but if one has any computation in mind then it's much better to skip the initial prenex step and introduce the Skolem (or Herbrand) functions directly. The reason it's better is precisely the subject of Frank's question and Carl's answer: The prenex step can convert two originally separate (unnested) quantifiers into a nested pair, which can mean that Skolem (or Herbrand) function symbols have more argument places than they should. Those extra arguments can considerably complicate the task of finding suitable unifications, a task that lies at the heart of many of the computational uses of Skolem and Herbrand forms.

Actually, the extra arguments can also cause trouble in a few purely theoretical situations, if one needs precise quantitative information. If I remember correctly, this sort of trouble is the root of the errors in Herbrand's original proof of his theorem (see "False Lemmas in Herbrand," Bull. A.M.S. 69 (1963) 699-706).

share|cite|improve this answer

Your Answer


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