Given ∀x.∀y.p(x,y), use the Fitch System to prove ∀x.∀y.p(y,x)

Question

In order to solve this question, I think I need to swap the two closed variables. I tried applying Universal Elimination in order to open up the closed variable but I don't know what to do after I reach- p(x,y).

Answer 1

This is one of those cases where it is clearest to use a Fitch-style system where we have to use a syntactically differentiated class of symbols for parameters (rather than re-cycle the same symbols for both [bound] variables and [unbound] parameters). For example, this is neat and clear:

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\forall x\forall yPxy} {\forall yPay\\ Pab\\ \forall yPyb\\ \forall x\forall yPyx} $

We instantiate the outer universal quantifier with a parameter at the second line, and then instantiate the quantifier at that line with a new parameter to get the third line. $a$ and then $b$ can be thought of as dummy names for arbitrarily chosen objects in the domain. Since they are arbitrary (don't appear in any assumption), we can then generalize (using any variable we like to form the universal quantifier) at the fourth line, and generalize again to get what we wanted at the fifth line. And so it goes.

If you use an (evil! ;) ND system that doesn't differentiate properly between bound variables and dummy names, then as Mauro says you'd need something that looks like

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \fitch{\forall x\forall yPxy} {\forall yPwy\\ Pwz\\ \forall yPyz\\ \forall x\forall yPyx} $

But to explain what that means, to explain what is going on here, you'll have to explain that $w$ and $z$ are playing a different role to the bound variables $x$ and $y$; and it is a good Fregean principle to use different styles of symbols for expressions playing different roles. That's why the first version of the proof, by those standards, counts as more logically perspicuous than the second version.