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:
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))$
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!
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)$$