3

I want to find the prenex form of the following formula:

$\forall x P(X) \rightarrow \neg (\forall xQ(x) \rightarrow \exists y R(y))$

I found:

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

Can someone verify whether this is correct? And, also, how can I verify myself that this is the correct answer?

  • There is no general way to check if your prenex is right! Imagine if there were! Every true statement has a prenex form $\top$, so you could just check if a statement has the prenex form $\top$ to prove any formula in mathematics. – DanielV Dec 10 '16 at 22:04
  • @DanielV Wouldn't it be that any necessarily true statement has Prenex form $\top$? So, mathematical truths don't have Prenex form $\top$ ... Unless they happen to express a logical truth. Also, first-order logic is complete, so there is a systematic method that will be such that if the answer is correct, then that method will eventually find out it is. – Bram28 Dec 10 '16 at 22:42
  • "True" in proof theory means provable with respect to a logic, any other definition is sophistry. FOL is complete wrt model theory (for what that's worth, nothing IMO), that doesn't make it decidable over the usual grammar. – DanielV Dec 10 '16 at 22:46

2 Answers2

3

First, your $\forall x P(X) \rightarrow \neg (\forall x(Q(x) \rightarrow \exists y R(y)$ has some missing parentheses ... I assume it is:

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

OK, the relevant Prenex Laws (where Q does not contain any free variable $x$) are:

1A. $Q \rightarrow \exists x P(x) \Leftrightarrow \exists x (Q \rightarrow P(x))$

1B. $Q \rightarrow \forall x P(x) \Leftrightarrow \forall x (Q \rightarrow P(x))$

1C. $\exists x P(x) \rightarrow Q \Leftrightarrow \forall x (P(x) \rightarrow Q)$

1D. $\forall x P(x) \rightarrow Q \Leftrightarrow \exists x (P(x) \rightarrow Q)$

And of course we have:

2A. $\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x) $

2B. $\neg \exists x P(x) \Leftrightarrow \forall x \neg P(x) $

2C. $\forall x P(x) \Leftrightarrow \forall x' P(x')$

2D. $\exists x P(x) \Leftrightarrow \exists x' P(x')$

So:

$\forall x P(X) \rightarrow \neg (\forall x Q(x) \rightarrow \exists y R(y)) \Leftrightarrow$ (2C)

$\forall x P(X) \rightarrow \neg (\forall x'Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1D)

$\forall x P(X) \rightarrow \neg \exists x'(Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1A)

$\forall x P(X) \rightarrow \neg \exists x' \exists y (Q(x') \rightarrow R(y)) \Leftrightarrow$ (2B * 2)

$\forall x P(X) \rightarrow \forall x' \forall y \neg (Q(x') \rightarrow R(y)) \Leftrightarrow$ (1B * 2)

$\forall x' \forall y(\forall x P(X) \rightarrow \neg (Q(x') \rightarrow R(y))) \Leftrightarrow$ (1D)

$\forall x' \forall y \exists x( P(X) \rightarrow \neg (Q(x') \rightarrow R(y)))$

So yes, if I place the parentheses correctly, then you are correct!

If, however, you meant:

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

then you get:

$\forall x P(X) \rightarrow \neg \forall x (Q(x) \rightarrow \exists y R(y)) \Leftrightarrow$ (2D)

$\forall x P(X) \rightarrow \neg \forall x' (Q(x') \rightarrow \exists y R(y)) \Leftrightarrow$ (1A)

$\forall x P(X) \rightarrow \neg \forall x' \exists y (Q(x') \rightarrow R(y)) \Leftrightarrow$ (2A + 2B)

$\forall x P(X) \rightarrow \exists x' \forall y \neg (Q(x') \rightarrow R(y)) \Leftrightarrow$ (1A + 1B)

$\exists x' \forall y (\forall x P(X) \rightarrow \neg (Q(x') \rightarrow R(y))) \Leftrightarrow$ (1D)

$\exists x' \forall y \exists x( P(X) \rightarrow \neg (Q(x') \rightarrow R(y))) $

Bram28
  • 100,612
  • 6
  • 70
  • 118
  • 1
    I think you have a mistake, the $\forall x'$ should include the $\exists y~ Ry$ in it's argument. That is, it is $\forall x'~ (Qx' \Rightarrow \exists y~Ry)$ instead of $(\forall x'~ Qx') \Rightarrow (\exists y~Ry)$. – DanielV Dec 10 '16 at 22:02
  • 1
    @DanielV The original sentence is missing some parentheses ... maybe we interpreted it differently. I indicated how I read it .. but maybe that's not what was meant. Hopefully the OP can add the missing parentheses – Bram28 Dec 10 '16 at 22:04
  • I edited the sentence. I'm sorry for this. What is the correct solution, as there seems to be confusion. –  Dec 10 '16 at 22:31
  • @Math_QED there is still one parentheses too few ... or too many. Anyway, it now looks more like it is the second solution ... In which case you had a small mistake in your answer. – Bram28 Dec 10 '16 at 22:36
  • I edited it again. It's not smart doing mathematics when tired. Now it's the correct sentence. –  Dec 10 '16 at 22:42
  • 1
    @Math_QED Aha! That's exactly what I thought it was ... So it is the first answer after all ... And so your answer is correct! – Bram28 Dec 10 '16 at 22:44
  • Well, that's a good thing! Thanks a lot for your help :) –  Dec 10 '16 at 22:54
2

Fast way:

$$\forall x ~Px \Rightarrow_1 \lnot \forall z~( Qz \Rightarrow_2 \exists y ~ Ry) $$

Count the number of $\lnot$s and $\Rightarrow$ that the quantifier is part of the condition of. If it is odd, change the quantifier to the other kind.

  • $\forall x$ is in the condition of $\Rightarrow_1$, so it gets changed
  • $\forall z$ is inside the $\lnot$ and is not part of the condition of any implication, (it is part of the consequence of $\Rightarrow_1$, but consequences don't count), so it gets changed
  • $\exists y$ is not part of the condition of any implications, it is in 1 $\lnot$, so it gets changed

So moving everything to the left and changing:

$$\exists x \exists z \forall y~(Px \Rightarrow \lnot (Qz \Rightarrow Ry))$$

You pull them out in a way that changes the order, which requires a more complicated approach.

For the updated question:

$$\forall x ~Px \Rightarrow \lnot (\forall z~ Qz \Rightarrow \exists y ~ Ry) $$

  • $\forall x$ is part of 1 condition and 0 negations, flipped.
  • $\forall z$ is part of 1 condition and 1 negation, not flipped
  • $\exists y$ is part of 0 conditions and 1 negation, flipped

$$\exists x \forall z \forall y~(Px \Rightarrow \lnot (Qz \Rightarrow Ry)) $$

DanielV
  • 23,556