# Simple Skolemization Question

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!

• 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?
– D.W.
Jul 15 at 19:01
• 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). Jul 15 at 19:04
• 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. Jul 15 at 21:14

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.