Proving formula in predicate logic Give a proof of $ \vdash (\forall x)(\forall y)x=y \rightarrow (\forall y)y=y$
How could i prove this one ?
 A: Reference to George Tourlakis, Mathematical Logic (2008), Chapter 4, Exercise 9, page 150 :


Give a proof of $\quad \vdash \forall x \forall y (x = y) \rightarrow \forall y (y = y)$.


We will use Logical Axiom Schemata of Predicate Logic (page 139). 
We will use the following tautology :

$\vDash_{TAUT} p \rightarrow (q \rightarrow p)$.

Our proof will start with the following instance of the above tautology (by Ax1) :

$\vdash \forall y (y = y) \rightarrow ( \forall x \forall y (x = y) \rightarrow \forall y (y = y))$

From the identity axiom (Ax5) : $x = x$ we will have the following axiom ("the set of logical axioms of first-order logic consists of all possible partial generalizations of the formulae in the following groups, Ax1-Ax6") :

$\vdash \forall y (y = y)$.

Finally, form the two formulas above, by modus ponens, we will have :


$\vdash \forall x \forall y (x = y) \rightarrow \forall y (y = y)$.



Bonus : Execise 8 :


Is $\forall x \forall y (x = y) \rightarrow \forall y (y = y)$ an instance of Ax2? Why?


Ax2, page 139, is : "This group contains all formulae of the form $\forall x A \rightarrow A[x : = t]$. It has the name specialization axiom but also substitution axiom".
Why we cannot apply Ax2 to the formula $\forall y (x = y)$ with the term $y$ as $t$ ? We would have as an "instance" of the axiom the formula :
$\forall x \forall y (x = y) \rightarrow \forall y (x = y)[x : = y]$, 
i.e. :
$\forall x \forall y (x = y) \rightarrow \forall y (y = y)$.
This instance of Ax2 is incorrect (see remark page 142) because with the substitution $x := y$ the term $y$ has been "captured" by the quantifier $\forall$, and this kind of substitution is not allowed (see page 133, for the explanation about substitution).
In conclusion, we cannot prove it from Ax2; so, we need another approach in order to prove it (see above), and we know that, being valid, the formula is provable, by completeness of first-order logic.
A: Here is a proof using natural deduction with a Fitch-style proof checker:

The inference rules used are universal elimination ($\forall$E), universal introduction ($\forall$I), and conditional introduction ($\to$I).

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
