I want to transform this formula:

$$(\forall a \exists b \exists c S(a,b) \land T(b,c)) \land (\neg \forall b U(b))$$

in Prenex normal form (PNF). Therefore, I do the following steps:

  1. Rename second b into d and remove neg: $(\forall a \exists b \exists c S(a,b) \land T(b,c)) \land ( \exists d \neg U(d))$

  2. Remove parentheses and bring quantors to the left: $\forall a \exists b \exists c \exists d S(a,b) \land T(b,c) \land ( \neg U(d))$

Now I have PNF, right?

Is there a special way to remove parentheses or something to consider? Is there a slower step by step approach available?

Thanks for your help!

  • $\begingroup$ You got the right answer, but you really should learn why the approach works, and when it doesn't. $\endgroup$ – DanielV Jul 3 '18 at 22:12
  • $\begingroup$ @DanielV thanks for fast reply. Do you have a good resource with some examples for me? $\endgroup$ – user3352632 Jul 3 '18 at 22:19
  • $\begingroup$ Prenex normal form is easy to search for, but really, I bet you could figure it out if you tried. $\endgroup$ – DanielV Jul 3 '18 at 22:20

$$\forall a \exists b \exists c \exists d ~S(a,b) \land T(b,c) \land (\neg U(d))$$

That is correct.   The first composite step, alpha-substitution and negation duality, is exactly how to handle having two bound $b$ variables when one is an existential.

The distribution of that quantifier is also handled well.   However, although you may leave them there if you so prefer, just as a matter of style, I'd also remove the parenthesis around the negated $U$, since they are unnecessary.   It is less cluttered that way.

$$\forall a\,\exists b\,\exists c\,\exists d\,~S(a,b) \land T(b,c) \land \neg U(d)$$

Now, durring the distribution step, you could alternatively have postioned the existential $d$ first.   Either way would be okay.

$$\exists d\,\forall a\,\exists b\,\exists c\,~S(a,b) \land T(b,c) \land \neg U(d)$$


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.