In predicate logic PL, I have learnt that we annot change the order of qualified quantifiers.
For instance, $(\forall x>0)(\forall y>x)P$ is not equivalent to $(\forall y>x)(\forall x>0)P$
But what should we put in the place of the question marks to make $(\forall y ?)(\forall x ?)P$ equivalent to $(\forall x>0)(\forall y>x)P$?
I know that maybe it is about $x$ ocurrs free in $(\forall y>x)$ in $(\forall y>x)(\forall x>0)P$, but it is bounded in $(\forall x>0)(\forall y>x)P$. Could someone please tell me some possible way to fix it?
I have worked on it for some time. May I also ask for some explaination as well. Thanks.
If the qualified $y$ makes reference to the $x$, as in $y >x$, you cannot swap the quantifiers as indeed you would get a free variable $x$. So ... something you can do is to not qualify the $y$ right inside the quantifier, but wait until the $x$ has been introduced. So, you could do:
$$(\forall y)(\forall x >0)(y >x \rightarrow P)$$
You could also un-qualify the $x$ ... for consistency sake:
$$(\forall y)(\forall x)((x>0 \land y>x) \rightarrow P)$$
The nice thing about unqualified quantifiers is that they can be freely swapped, as long as they are of the same type and next to each other.
On the other hand, if you don't like the extra parentheses, you could do:
$$(\forall y)(\forall 0 < x<y) P$$