What is(are) the problem(s) in trying to prove $y+x\le x+y$ from $\forall x\forall y(y+x\le x+y)$ by "spec"?

Question

In the image below from Angelo Margaris's book First Order Mathematical Logic,

Regarding the image above from Angelo Margaris's book First Order Mathematical Logic I have the following questions,

1. Can someone explain to me the problems that Margaris is referring to if we try to prove $(2)$ from $(1)$ by spec?

2. Why this problem is referred to as being purely notational?

3. If $\forall v P$, we can always deduce $P$ because $P$ always admits $v$ for $v$. But then why can't the same reasoning be applied (twice) to the case in question?

By the way, I think I understand how Margaris overcomes the said difficulty. But I am wondering, what was the need for it.

Here "spec" is the following rule,

If $Δ$ be a set of formulas and $Δ⊢∀ v P$ then $Δ⊢P(t/v)$ provided that $P$ admits $t$ for $v$ (where $t$ is a term).

---

Notes:

The only axioms and rule of inference that I can use are,

$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$

$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$

$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$

$\color{crimson}{\text{Axiom 4.}}\ \forall v(P\to Q)\to(\forall v P\to\forall v Q)$

$\color{crimson}{\text{Axiom 5.}}\ \forall vP\to p(t/v)$ provided $P$ admits $t$ for $v$.

$\color{crimson}{\text{Axiom 6.}}\ P\to \forall vP$ provided $v$ is not free in $P$.

$\color{crimson}{\text{Axiom 7.}}$ If $P$ is an and $v$ is free in $P$ then $\forall v P$ is also an axiom.

$\color{crimson}{\text{Rule of Inference.}}$ Modus Ponens.

Answer 1

When we specialise a universally quantified theorem $\forall vP$, we want to avoid variables in the term $t$ that we are substituting for $v$ in $P$ being "captured" by quantifiers inside $P$. In your example, $P$ is $\forall x\forall y(x + y \le y + x)$, $t$ is $y$ and $v$ is $x$. If we did the substitution naively, we would get $\forall y(y + y \le y + y)$: a true statement, but too weak to deliver what we want, namely $y + x \le x + y$.

In your example, the naive approach gives a statement that is true but too weak. However, if we started with the true statement $P \equiv \forall y \exists x(x > y)$ and naively substituted $x$ for $y$, we would get the false statement $\exists x(x > x)$.

The specialisation rule as you have quoted it includes a side-condition requiring that $P$ admits $t$ for $v$ which is intended to prevent the rule being applied if variable capture would occur. Other presentations of first-order logic say that bound variables should be renamed as necessary to avoid variable capture when performing the substitution.

Answer 2

1. I think it's pretty much what @fleablood commented on the post. If you use spec on $\forall x \forall yP(x,y)$, it ends up being $\forall x P(x,x)$, and you can't "recover" $y$'s space as a variable. That is, if you tried to use spec again on that formula, to make $x$ become $y$, it'd turn out as: $\forall y P(y,y)$

2. The problem is referred to as pure notational because this would't have happened if $(2)$ had been written with other variables. E.g. Using spec, $\forall \alpha \forall \beta(\alpha +\beta\leq\beta+\alpha)$, becomes $\forall \alpha \forall x(\alpha +x\leq x+\alpha)$, and using spec once again, $\forall y \forall x(y+x\leq x+y)$.

3. Because of the variable change, as in point 1.