[Math] Equivalence vs equisatisfiability

logicmodel-theory

Wikipedia page states that first order formula after skolemization is equisatisfiable but not equivalent to original one. I do not understand what the difference is. Here is Wikipedia's definition:

Two formulae are equisatisfiable if either both formulae are
satisfiable or both are not. Two equisatisfiable formulae may have
different models. As a result, equisatisfiability is different from
logical equivalence, as two equivalent formulae always have the same
models.

Question is how can it be that something is not equivalent but equisatisfiable.

Best Answer

In oder to "manufacture" a counterexample for two formuale being equisatisfiable but not equivalent, consider the first-order language of arithmetic with the predicate $<$ ("less-than") and a new (unary) function symbol $f$, and let :

$\phi := \forall x \exists y (x < y), \psi := \forall x (x < f(x))$.

The two are satisfiable in the same model, considering $\mathbb N$ and interpreting $<^N = <$ and $f^N: \mathbb{N} \to \mathbb{N}$ being the addition $x \mapsto x+1$.

However, they are not equivalent, i.e. there is another model where one is true and the other is not: consider again $\mathbb N$ and interpret the function symbol $f$ with : $f^N : \mathbb N \to \mathbb N$ such that $f^N(n)=0$, for all $n \in \mathbb N$. In this model, $x < f(x)$ is false.

In fact: $\forall x (x < f(x)) \vDash \forall x \exists y (x < y)$ but $\forall x \exists y (x < y) \nvDash \forall x (x < f(x))$.

Related Question