0
$\begingroup$

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...

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.