= Solution
The usual transformation to <clausal normal form> preserves $\boxed{\text{equisatisfiability, but not necessarily logical equivalence}}$. Removing implications and distributing <logical conjunction> and <logical disjunction> preserve <logical equivalence>. <Skolemization> introduces new symbols and chooses witnesses as functions of preceding universally quantified variables.
For example,
$$
\varphi=\forall x\exists y\,R(x,y)
\quad\longmapsto\quad
\psi=\forall x\,R(x,f(x)).
$$
On the domain $\{0,1\}$, let $R$ be equality. Then $\varphi$ is true. Expand this same <first-order structure> by interpreting $f$ as the constant function with value $0$. The resulting <first-order structure> falsifies $\psi$ at $x=1$. Interpreting $f$ as the identity instead satisfies $\psi$.
Thus every model of $\psi$ has a reduct satisfying $\varphi$, and a model of $\varphi$ can be expanded with suitable witnesses to satisfy $\psi$. That model-expansion property gives <equisatisfiability>, not <logical equivalence> for every interpretation of the added function. If “CNF” means a conjunctive matrix with existential quantifiers retained, <Skolemization> has not yet happened and an equivalent form is possible; this is why the convention must be specified.
Back to article page
