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:
$\phi$(x,f(x))
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?
Best Answer
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.