# Translation of a mathematical statement formulated in words to one formulated in predicate logic

I want to express the fact that for all $x \in A$ that have the property that for all $y\in x$ $T(x,y)$ is true and there exists an $u \in B$ such that $P(y,u)$ is true AND for all $v\in C$, $Q(y,v)$ and $R(x,v)$ are also true, then $S(x)$ is true.

(Note that this statement is just a toy statement I have invented, because I was not sure I understood this transformation well, so I wanted to make it difficult, keeping with the idea, that if I got this difficult one right, that I probably understood how to do the transformations)

Formulated in a formal language of predicate logic, would this be

$$\forall x ( x\in A \land \ \ \forall y (y\in x \rightarrow \ ( T(x,y) \land \ldots$$ $$\ldots \land ( \exists u ( u \in B \land P(y,u) \land \forall v ( v\in C \rightarrow ( Q(y,v) \land R(x,v)))))))\rightarrow S(x) )$$

(hope I didn't forget any paranthesis...) ?

Is there also a way to move the quantifiers "$\forall$" at the front, so that that string starts with $\forall x \forall y \ldots$ ?

-
All quantifiers can be moved to the front. However, we cannot in general move the universal quantifiers to the front, to be followed by the existential quantifiers. (I am assuming that we will not introduce additional function symbols to the language.) –  André Nicolas Jul 15 '11 at 18:27

Edit: As Carl reminded me, logically equivalent prenex forms can (contrary to what I originally wrote) begin with different quantifiers: $\forall x \exists y(\phi(x) \land \psi(y))$ and $\exists y \forall x (\phi(x) \land \psi(y))$ are both prenex forms of $\forall x \phi(x) \land \exists x \psi(x)$. However, the order of the quantifiers can also matter: $\forall x \exists y \phi(x,y)$ and $\exists y \forall x \phi(y,x)$ are not logically equivalent. And it is certainly not possible in general to bring all of the universal quantifiers to the front.
@temo: Yes (unless I miscounted parentheses). However, since $u$ doesn’t appear after ‘AND’, it might be more natural to write $\dots \land (\exists u(u\in B \land P(y,u)) \land \dots \land R(x,v))))))\to S(x))$, limiting the scope of $\exists u$ to $u\in B \land P(y,u)$. –  Brian M. Scott Jul 15 '11 at 19:55
It isn't true that all the prenex normal forms must have the same classification, e.g. $(\forall x) P \land (\exists y) Q$ can be put in either $\forall \exists$ or $\exists \forall$ form. –  Carl Mummert Jul 15 '11 at 23:10
@ Brian M. Scott ok, thanks, good remark about the scope of $u$ –  temo Jul 16 '11 at 8:44