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 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.