# 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, 2022 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, 2022 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, 2022 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.