I am to solve this problem:

$ \exists y \forall x \neg P(x,y) \rightarrow \forall x \exists y Q(x,y) $

I'm getting rid of implication:

$ \forall y \exists x P(x,y) \lor \forall x \exists y Q(x,y) $

Am I right that we have to resolve varialbe conflict this way: x->t and y->k

$ \forall y \exists x P(x,y) \lor \forall t \exists k Q(t,k) $

Then I'm moving all quantifiers to the front

$ \forall y \exists x \forall t \exists k (P(x,y) \lor Q(t,k) ) $

Now getting rid of exists-quantifiers x=f1(y) and k=f2(y,t). I'm a bit confused to change new variable k to the function.

$ \forall y \forall t (P(f1(y),y) \lor Q(t,f2(y,t))) $

Am I right at my solution?

  • $\begingroup$ @DerekElkins, you are right, they should be different $\endgroup$ – Elvin Aug 11 at 19:08
  • 1
    $\begingroup$ Minor issue: $t$ and $k$ are unusual names to choose for variables - more conventional would be $x, y, z, u, v, w$ (in about that order of frequency). $\endgroup$ – lemontree Aug 12 at 13:40

If your question is whether it's legitimate to change a recently renamed variable for an existential quantifier into a function symbol - sure, there's nothing wrong about that; there is no difference in whether the variable name has been changed at some point or not; the elimination of $\exists$ is independent of that step.

  • $\begingroup$ ok, so my solution is right ? $\endgroup$ – Elvin Aug 12 at 12:33
  • 1
    $\begingroup$ @Elvin Yes, it looks correct. $\endgroup$ – lemontree Aug 12 at 13:39

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.