Symmetry of Predicate and Universal Quantifiers

Question

$$ \forall x \forall y P(x,y) \implies \forall x \forall y P(x,y) \land P(y,x) $$

I guess the above statement is valid but no idea how to formally prove it, any idea?

Answer 1

Basically: First use universal elimination (/instantiation) of $x$ and $y$ to arbitrary constants $c$ and $d$, to give $P(c,d)$.   Then because the premise is still available use universal elimination on it again, but replacing $x$ and $y$ with the (now) existing constants $d$ and $c$, to obtain $P(d,c)$.   Then use conjunction introduction on these two statements, and finish with universal introduction (/generalisation) of the (still) arbitrary constants back to $x$ and $y$. $$\begin{array}{l|l:l} 1. & \forall x\forall y\;P(x,y) \\ \quad 2. & \forall y\;P(c,y) & 1,\forall\mathsf E \mid^x_c\\ \qquad 3. & P(c,d) & 2,\forall\mathsf E \mid^y_d \\ \qquad 4. & \forall y\;P(d,y) & 1,\forall\mathsf E \mid^x_d \\ \qquad 5. & P(d,c) & 4,\forall\mathsf E \mid^y_c \\ \qquad 6. & P(c,d)\wedge P(d,c) & 3,5,\wedge\mathsf I \\ \hline \quad 7. & \forall y\;(P(c,y)\wedge P(y,c)) & 6,\forall \mathsf I^d_y \\ \hline 8. & \forall x\forall y\;(P(x,y)\wedge P(y,x)) & 7, \forall\mathsf I^c_x \\ \hline \end{array} \\\therefore \forall x\forall y\;P(x,y)\;\vdash\; \forall x\forall y\;\big(P(x,y)\wedge P(y,x)\big)\\ \Box$$

---

$$\dfrac{\dfrac{ \dfrac{\forall x\forall y\;P(x,y) }{ P(c,d) }\quad \dfrac{\forall x\forall y\;P(x,y) }{ P(d,c) } }{ P(c,d)\wedge P(d,c) } }{ \forall x\forall y\;\big(P(x,y)\wedge P(y,x)\big) }$$