Proving formula in predicate logic

Question

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

How could i prove this one ?

Answer 1

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.