I asked in another question when is it appropriate to de-Skolemize a statement. The answer, I'm not sure I'm satisfied with yet, relies on a second order logical equivelance, but Skolem normal form isn't logically equivalent. I've read first order Skolemization can be defined through a second order logic equivelance:

$\forall$x$\exists$y $\phi$(x,y) $\iff$ $\exists$F$\forall$x $\phi$(x,F(x))

From this we can omit the quantifiers, and treat all variables as implicitly universally quantified:


I also understand that Skolem normal form is equisatisfiable:

$\forall$x$\exists$y $\phi$(x,y) $\vDash$ $\phi$(x,f(x))

[I apparently incorrectly understood it, see accepted answer]

But apparently this is not equivalent.

What does this mean? Can we freely move between Skolem normal form and the second order sentence even though they aren't equivalent? I only see equisatisfiability with Skolemization used to prove satisfiability or unsatisfiability, and I haven't seen it used to prove logical consequence from first order formulas except through unsatisfiability with searching for a contradiction.

Why is the second order form of a first order sentence that moves existential quantifiers out of scope of universal quantifiers logically equivalent, while Skolem normal form only equisatisfiable?


It's perhaps best to think about this first in the context of a particular structure and a particular formula, where you can easily see what's going on. Consider the structure of the natural numbers with the usual ordering relation $<$. The sentence $\forall x\exists y\,(x<y)$ is true in this structure, because for every natural number $x$ there is a larger one $y$, for example $x+1$ (or $x+17$ or $(2x)!$ or lots of other choices). Equivalently, the second-order sentence $\exists F\forall x\,(x<F(x))$ is true in the same structure, witnessed by functions like $F(x)=x+1$ (or $F(x)=x+17$ or $F(x)=(2x)!$, or lots of other functions $F$).

On the other hand, we cannot say (as you did) that $\forall x\exists y\,(x<y)\models\forall x\,(x<F(x))$. To see this, notice first that this "logical consequence" relationship concerns structures for a language that has not only the relation symbol $<$ but also the function symbol $F$. Consider the structure of natural numbers with $<$ as before and some interpretation of the function symbol $F$. Then $\forall x\exists y\,(x<y)$ is true (regardless of the interpretation of $F$ because it doesn't mention $F$), but whether $\forall x\,(x<F(x))$ is true depends on how we interpret $F$. It's true if we take $F(x)=x+1$ (or $F(x)=x+17$ or $F(x)=(2x)!$, or lots of other functions $F$), but it's false if we take $F(x)=0$ (or $F(x)=17$ or $F(x)=\lfloor x/2\rfloor$, or lots of other functions). But $\models$ means that every structure satisfying what's on the left of $\models$ also satisfies what's on the right. So in our case, it would require that $\forall x\,(x<F(x))$ is true regardless of how we interpret $F$ as long as $\forall x\exists y\,(x<y)$ is true. Since that doesn't hold when $F$ is "badly" interpreted ($0$ or $17$ or $\lfloor x/2\rfloor$), we don't have $\forall x\exists y\,(x<y)\models\forall x\,(x<F(x))$. The most we can say is that, having satisfied $\forall x\exists y\,(x<y)$, we can, by suitably interpreting $F$, also satisfy $\forall x\,(x<F(x))$ --- and vice versa. That's what "equisatisfiable" means.

  • $\begingroup$ I take it this means you can always reintroduce the second order existential quantifier of the function to restore logical equivalence... and then move the existential quantifier inside the universal quantifier to restore it to a first order formula. $\endgroup$ – dezakin Oct 18 '14 at 23:08
  • 1
    $\begingroup$ Reintroducing the second-order quantifier (or several of them, in more complicated cases) will convert "satisfiable" to "true". Moving the second-order quantifier inside the universal quantifier to return to first order is OK if the formula you're working with originally came from Skolemizing a first-order formula, but in general, starting with an arbitrary second-order existential formula, there will be no way to reduce it to an equivalent first-order formula. $\endgroup$ – Andreas Blass Oct 19 '14 at 3:01
  • $\begingroup$ Why can't you convert arbitrary second order formulas? I thought the second order equivalence relation implies both ways. If you can't convert arbitrary second order formulas, does that mean the answer to the linked question (about deskolemizing sentences produced from inferences on Skolemized statements) is incorrect? Or is converting something defined explicitly as a 'Skolem function' always allowed? $\endgroup$ – dezakin Oct 19 '14 at 6:40
  • 1
    $\begingroup$ As far as I can see, the linked answer is only about the case of second-order sentences obtained by Skolemizing first-order ones, not about general second-order sentences. It's not clear to me how you would even try to go about "de-Skolemizing" something that wasn't obtained by Skolemization in the first place. What if, for example, the function symbol $F$ that you want to get rid of has different arguments at different places in your second-order formula? $\endgroup$ – Andreas Blass Oct 19 '14 at 11:28

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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