Prove there's no algorithm which gets $\varphi$, a formula without free-variables as in input and returns a formula of the form $\varphi ' =\exists x_1,\ldots,\exists x_n \psi$ where $\psi$ is a formula without quantifiers such that $\varphi$ is satisfiable iff $\varphi$' is satisfiable.
Note: There's an algorithm for satisfiability of a formula without quantifiers and free variables.
I should get a contradiction with Church thesis somehow.
I'd be glad for help.