# Building an algorithm to build a satisfiable formula from a valid existential statement

Question:

Given the following signature - $\Sigma := \lbrace R^2, P^2, c\rbrace$ (2 relations and a constant), prove/disprove: There exists an algorithm that given an existential statement $\phi$ builds a formula $\psi$ with no quantifiers s.t. $\phi$ is valid $\iff \exists z \forall y \exists x \psi$ is satisfiable.

My answer: I believe this is true, but I'm not sure about it, would like to verify my algorithm:

1. We've seen that for any formula $A^\exists$ is valid $\iff$ $A$ is satisfiable: therefore I'll remove all $\exists$ quantifiers from $\phi$ and call it $\phi'$ - it's satisfiable $\iff \phi$ is valid.
2. I'll rename variables in $\phi'$ s.t. their names won't be x,y,z.
3. I'll add the required quantifiers to $\phi'$: $\phi''=\exists z \forall y \exists x \phi'$ . Since these 3 new variables don't appear in the new formula, it's equivalent logically to $\phi'$.

This seems like too simple of a solution to be right...

• Do you mean to say "$\phi$ is valid $\iff$ $\exists z \forall y \exists x \psi$ is satisfiable"? Otherwise how is $\psi$ used? – Dan Simon Feb 19 '16 at 15:03
• fixed the question. – jreing Feb 22 '16 at 10:22