Let there be some formula $\phi$, is there an algorithm to construct a closed formula $\phi'=\exists x_1...\exists x_n \psi$ where $\psi$ does not have any quantifiers and $\phi$ is satiable iff $\phi'$ is satiable?
My idea is that it is wrong, and if we assume that it is true, then we can convert $\phi '$ to Skolem normal form to a closed formula $\phi ''$ with no quantifiers, so if we look at Herbrand's theorem, we only have one closed instance of $\phi ''$ which is the formula itself so we have an always halting algorithm to check whether a formula is satiable in first order logic. Is there any theorem that says the language of satiable FOL formulas is undecidable or something like that?
thanks.
edit: I found in Wikipedia that validity is undecidable and you can solve validity of $\phi$ by checking that $\lnot \phi$ is not satiable, so I guess this solves it. If anyone can comment whether I made a mistake along the way I'd appreciate it.