# Construct skolemform of: $\forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$

This question is not asking for a solution, but rather as a check / validation of my thought process.

Given the form: $W = \forall X.((\forall Y.\exists Z. R(X,Y,Z)) \land \forall S. \exists T. R(X, S,T))$

The algorithm I learnt states, that I have to 1th bring $W$ into prenex form. Doing so I bring all quantors to the beginning, if necessary resolve all variable dependencies by defining fresh variables. The exact sequence of the operators has to be maintained in the process!

2th I look for something of the form: $\forall x_1. \forall x_2. \forall x_3 \dots \exists y_1 \exists y_2 (R(y_1, y_2))$ and replace it by something like $\forall x_1. \forall x_2. \forall x_3 (R(g(x_1, x_2, x_3, \dots), f(x_1, x_2, x_3, \dots)))$

In the above example $W$, following strictly the rules stated previously, I would expect the result:

Prenexform: $\forall X.\forall Y. \exists Z. \forall S. \exists T. (R(X,Y,Z)) \land R(X, S,T))$

Skolemform: $\forall X.\forall Y. \forall S. (R(X,Y,g(X,Y)) \land R(X, S,f(X,Y,S))$, which might be correct, but kinda dumb looking.

Thus the question arises, if the rules above are absolut, if there were not a way to soften them and for example allow to switch the order of $\forall$ and $\exists$ operators.

Any constructive comments/answers to my question are appreciated.

• The formula defining $W$ is ill-bracketed. That makes it a bit difficult to be sure what exactly you have in mind. – Martin Berger Mar 27 '17 at 10:29
• @MartinBerger, fixed the brackets. – Imago Mar 27 '17 at 10:32
• The Skolem-function $f$ only needs two arguments, $X$ and $S$, for $Y$ isn't 'active' in the existential quantification of $T$. – Martin Berger Mar 27 '17 at 10:39
• Yeah, I thought so - but how do you justify that given the prenex form? I don't see how to build the prenex in a way that both $f$ and $g$ just take two arguments - that was the whole point of the example chosen above. – Imago Mar 27 '17 at 10:50
• OK, I see the issue now. This is related to the problems leading to independence-friendly logic, see here and here. – Martin Berger Mar 27 '17 at 11:02