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.

  • $\begingroup$ The formula defining $W$ is ill-bracketed. That makes it a bit difficult to be sure what exactly you have in mind. $\endgroup$ – Martin Berger Mar 27 '17 at 10:29
  • $\begingroup$ @MartinBerger, fixed the brackets. $\endgroup$ – Imago Mar 27 '17 at 10:32
  • $\begingroup$ The Skolem-function $f$ only needs two arguments, $X$ and $S$, for $Y$ isn't 'active' in the existential quantification of $T$. $\endgroup$ – Martin Berger Mar 27 '17 at 10:39
  • 2
    $\begingroup$ 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. $\endgroup$ – Imago Mar 27 '17 at 10:50
  • 1
    $\begingroup$ OK, I see the issue now. This is related to the problems leading to independence-friendly logic, see here and here. $\endgroup$ – Martin Berger Mar 27 '17 at 11:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.