1. ## Reversing quantifiers

Any hints on the strategy to derive ∃y∀x(Ax & By) from ∀x∃y(Ax & By) in fitch-format? I've been stuck on this one for weeks.

2. ## Re: Reversing quantifiers

"There exists x (property of x)" can be changed to "not For all x, not (property of x)." Same thing in converse. Is that enough of a hint?

3. ## Re: Reversing quantifiers

Originally Posted by Annatala
"There exists x (property of x)" can be changed to "not For all x, not (property of x)." Same thing in converse.
Yes, but I am not sure how this helps here.

Starting from $\displaystyle \forall x\exists y\,(Ax\land By)$, we can instantiate x with an arbitrary term t (e.g., a fresh variable) and get a y such that $\displaystyle At\land By$, in particular, $\displaystyle By$. So, we are left to show $\displaystyle \forall x\,(Ax\land By)$. Fix an arbitrary x, instantiate the universal variable in $\displaystyle \forall x\exists y\,(Ax\land By)$ with x and thus get $\displaystyle Ax$.

4. ## Re: Reversing quantifiers

Emakarov, I'm not sure it's that easy to do in a fitch-format derivation. A violation of rules involving the eigen-variable occur. So, for example, I can't do this:
∀x∃y(Ax & By)
∃y(Az & By)
-Az&Bw
-Az
-∀xAx

('-' indicates a sub-derivation). The last line in the sub-derivation is a violation. I can't universally quantify anything that's free in an assumption.

5. ## Re: Reversing quantifiers

Here is a derivation in tree format.

$\dfrac{\raisebox{\depth}[\totalheight][0pt]{\dfrac{\forall&space;x\exists&space;y\,(Ax\land&space;By)}{\exists&space;y\,(Az\land&space;By)}}\quad\raisebox{\depth}[\totalheight][0pt]{\dfrac{\dfrac{\dfrac{\raisebox{\depth}[\totalheight][0pt]{\dfrac{\raisebox{\depth}[\totalheight][0pt]{\dfrac{\forall&space;x\exists&space;y\,(Ax\land&space;By)}{\exists&space;y\,(Az'\land&space;By)}}\quad&space;\raisebox{\depth}[\totalheight][0pt]{\dfrac{\overset{(2)}{Az'\land&space;Bw'}}{Az'}}}{Az'}{\scriptstyle(2)}}\quad\raisebox{\depth}[\totalheight][0pt]{\dfrac{\overset{(1)}{Az\land&space;Bw}}{Bw}}}{Az'\land&space;Bw}}{\forall&space;x\,(Az\land&space;Bw)}}{\exists&space;y\forall&space;x\,(Ax\land&space;By)}}}&space;{\exists&space;y\forall&space;x\,(Ax\land&space;By)}{\scriptstyle(1)}$

6. ## Re: Reversing quantifiers

Originally Posted by emakarov
Yes, but I am not sure how this helps here.
My bad. I don't understand this question at all, although I thought I did.