Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m confused because the signature ends up changing when fresh functions are added (when you remove the for-all quantifiers), so how come the skolem form is equisatisfiable with the original formula if the signatures have changed? Any help is appreciated!

  • $\begingroup$ I'm having a hard time parsing your first sentence/question. It has both an "if" and "iff", which is confusing me. Can you break it down into smaller parts, or use mathematics or parentheses to clarify the binding? $\endgroup$
    – D.W.
    Jul 15, 2022 at 19:01
  • $\begingroup$ Hi I added parentheses to clarify it: I just mean that, given F and G that are two FOL formulae under a signature S, F and G are said to be equisatisfiable if (F is satisfiable under S <=> G is satisfiable under S). $\endgroup$ Jul 15, 2022 at 19:04
  • $\begingroup$ What is the problem precisely? The statement about equisatisfiability under the same signature says nothing about equisatisfiability under two different signatures. There is no problem here. $\endgroup$ Jul 15, 2022 at 21:14

1 Answer 1


I'm assuming we're talking about classical first-order logic here.

Consider two sets of formulas $\Gamma$ and $\Lambda$. If $\Gamma$ and $\Lambda$ are equisatisfiable, it means that $\Gamma$ has a model iff $\Lambda$ has a model. They don't even have to be the same model! So it's a pretty weak condition. And it's what allows two theories with different signatures to be equisatisfiable.

By the Soundness and Completeness theorems, we have for any $\Gamma$ that $\Gamma$ is satisfiable iff $\Gamma$ is consistent. From this we can conclude that if $\Gamma$ and $\Lambda$ are equisatisfiable, then $\Gamma$ and $\Lambda$ are equiconsistent.

So in the case of Skolemization, we've reduced the problem of equisatisfiability to the problem of equiconsistency. So all that's left is to show that Skolemization doesn't introduce any inconsistency.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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