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:
- 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.
- I'll rename variables in $\phi'$ s.t. their names won't be x,y,z.
- 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...