This question is motivated by this one, though more general.
Let $\phi$ be a formula in first order logic (w/o equality) over alphabet $S$ that contains no function symbols. Say $\phi$ is in prenex normal form $\phi = \forall x_1\cdots\forall x_n\exists y_1\cdots\exists y_m.\phi'$, where $\phi'$ is quantifier-free.
Question. Is there a formula $\psi$ that is satisfiable iff $\phi$ is, such that
- $\psi = \forall z_1\cdots\forall z_l. \psi'$ with $\psi'$ quantifier-free, and
- $\psi$ contains no function symbols.
I know that with only the first condition, $\psi$ is the Skolem normal form of $\phi$, but Skolemization comes at the cost of introducing new functions.
Edit: Of course, I don't know whether $\phi$ is satisfiable or not. Probably, I want to use $\psi$ to decide $\phi$'s satisfiability.
Terminology: A formula like $\phi$ is called a $\forall\exists$-formula (or sometimes an inductive formula). A formula like $\psi$ is called a $\forall$-formula (or a universal formula) with no function symbols.
The question you have asked is not the one you meant to ask.
The answer is yes: If $\phi$ is satisfiable, let $\psi$ be $\forall x\,(x = x)$, which is satisfiable. If $\phi$ is not satisfiable, let $\psi$ be $\forall x\, \lnot (x= x)$, which is not satisfiable.
I suspect what you really want is an equivalent formula. That is, you want to pick $\psi$ so that for every model $M$, we have that $\phi$ is true in $M$ if and only if $\psi$ is true in $M$ (and if $\phi$ and $\psi$ have free variables, we should say that for every model $M$ and every tuple $a$ from $M$ of the appropriate length, $M\models \phi(a)$ if and only if $M\models \psi(a)$).
The answer to this question is no. It's a basic fact of model theory that the truth of $\forall$-formulas is preserved under substructure. So if $\psi$ is a $\forall$-sentence, $M\models \psi$ is a model, and $N$ is a substructure of $M$, then $N\models \psi$ (if this isn't clear to you, you should try to prove it - it's not hard). And if there are no function symbols in the language, then any subset of $M$ is the domain of a substructure.
Now for a counterexample, we can take $\varphi$ to be the $\forall\exists$-sentence $\forall x\, \exists y\, \lnot (x = y)$. Suppose for contradiction that $\varphi$ is equivalent to a $\forall$-sentence $\psi$ with no function symbols. Let $M = \{a,b\}$ be a set of size $2$. Then $M\models \varphi$, so $M\models \psi$. Let $N = \{a\}$ be a substructure of $M$ of size $1$. Since $\psi$ is universal, $N\models \psi$, but also we can see that $N\not\models \varphi$, contradicting equivalence of $\varphi$ and $\psi$.
Your question was originally motivated by trying to express the group axioms by $\forall$-sentences without function symbols. The same argument shows that this is impossible: If the group axioms were expressible by $\forall$-sentences without function symbols, then every subset of a group $G$ would be a subgroup of $G$.