Prove that universal quantifiers commute: ∀x∀y p(x,y) ⟺ ∀y∀x p(x,y)

[amilapsn]

Homework Statement

This question may seem as an axiom to some. I also feel the same.
Prove:
$\forall x\forall y\ p(x,y)\Leftrightarrow\forall y\forall x\ p(x,y)$

The Attempt at a Solution

[/B]
$Assume\ \forall x\forall y\ p(x,y)$
$Let\ x_0\in \mathbb{R}$
$\ \ \therefore \ \forall y \ p(x_0,y)$
$\ \ Let\ y_0\in \mathbb{R}$
$\ \ \ \ \therefore\ p(x_0,y_0)$

From here onwards I'm stuck. Someone please help me to prove this (using only algebraic methods).

 

[WWGD]

Homework Statement

This question may seem as an axiom to some. I also feel the same.
Prove:
$\forall x\forall y\ p(x,y)\Leftrightarrow\forall y\forall x\ p(x,y)$

The Attempt at a Solution

[/B]
$Assume\ \forall x\forall y\ p(x,y)$
$Let\ x_0\in \mathbb{R}$
$\ \ \therefore \ \forall y \ p(x_0,y)$
$\ \ Let\ y_0\in \mathbb{R}$
$\ \ \ \ \therefore\ p(x_0,y_0)$

From here onwards I'm stuck. Someone please help me to prove this (using only algebraic methods).

Do you have a rule for existential generalization to conclude first $\forall x p(x,y_0)$ and then do the same for $y_0$?

 

[amilapsn]

Do you have a rule for existential generalization to conclude first $\forall x p(x,y_0)$ and then do the same for $y_0$?

I didn't get you...
Do you mean this...?

$Assume\ \forall x\forall y\ p(x,y)$
$Let\ y_0\in \mathbb{R}$
$\ \ \therefore \ \forall x \ p(x,y_{0})$
$\ \ Let\ x_0\in \mathbb{R}$
$\ \ \ \ \therefore\ p(x_0,y_0)$
$\ \ \therefore \forall x\ p(x,y_0)$
$\therefore \forall y\ \forall x\ p(x,y)$

BTW: I don't know what existential generalization could do here. Universal specification and universal generalization are the only rules of inference I can think of.
Thank You.

 

[amilapsn]

Somebody tell me whether I'm right or wrong...

 

[WWGD]

Could you please tell us the details of the rule of universal generalization that you use?

 

[amilapsn]

universal generalization:if P(a) is true for all a in universe of discourse then we can say $$\forall x P(x)$$

 

[WWGD]

Then it seems like from $p(x_0,y_0)$, since each of $x_0,y_0$ is arbitrary, you could generalize to either $\forall x p(x,y_0)$ or $\forall y p(x_0,y)$ and then generalize again. I think that does it.

 

[amilapsn]

Then it seems like from $p(x_0,y_0)$, since each of $x_0,y_0$ is arbitrary, you could generalize to either $\forall x p(x,y_0)$ or $\forall y p(x_0,y)$ and then generalize again. I think that does it.

Me too...