Question:
Prove/ disprove: there exists a finite runtime algorithm s.t given a formula $\phi=\exists x_1...x_n \forall y_1 ... y_n A$ that checks the satisfiability of $\phi$ when A is a formula with no quantifiers, function symbols or equality relation.
My answer I believe this is false (after a week of believing that it's true). So now I want to make sure, how about this proof:
A reduction to Church's theorem:
Given a general formula A
Assume by contradiciton that such algorithm $Z$ exists.
$A$ is satisfiable $\iff A^\forall$ is satisfiable $\iff \exists x_1 ... x_n A ^\forall=\psi $ is satisfiable, (when the x's are new variables that didn't appear in $A$ before, I'm allowed to change the name of variables prior to this step if needed).
Now $Z(\psi)$ can solve the general satisfiability problem in contradiction with Church's theorem.
This is the Bernays-Schönfinkel theorem. To decide whether your formula $\phi=\exists x_1...x_n \forall y_1 ... y_m A$ is satisfiabie, note that it is satisfiable iff it has a model with at most $n$ elements (because, as we have disallowed function symbols, we can discard elements other than the witnesses for the $x_i$ without invalidating $\phi$). It is a finite problem to decide whether $\phi$ has a model with at most $n$ elements.
[Your argument breaks down because $A$ is not an arbitrary formula here.]