# Is this transformation process of a predicate logic formula into Prenex normal form correct?

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?

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