Equivalence vs equisatisfiability

5k Views Asked by At

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.

1

There are 1 best solutions below

2
On 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))$.