# 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”?

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.

• I think the idea is that you can't replace $x$ with $y$ or $y$ with $x$ both at the same time and you can't replace them one at a time ($\forall x\forall yx+y\le y+x \implies\forall xx+x \le x+x \not \implies \forall x\forall y y+x \le x+y$). I think. The actual solution would be $\forall x\forall y x+y\le y+x\implies \forall x\forall z x + z\le z + x\implies \forall y\forall z y + z \le z + y\implies \forall y\forall x y+x \le x + y$ is okay. But that's not "by spec". (Bit unfair for him to use a vague term like "by spec" without formal definition in a book about formal logic.) – fleablood Sep 15 '18 at 15:19
• @fleablood: I have edited the question. – user170039 Sep 15 '18 at 15:22
• Presumably "$P$ admits $t$ for $v$" means that no free occurrence of $v$ in $P$ occurs in the scope of a quantifier binding a variable that appears free in $t$. So the given rule is not applicable in the case given. – Rob Arthan Sep 15 '18 at 16:00
• Well, the book says "try it" so have you tried it? If you had trouble what were they? If you didn't, post your results and people (who maybe know logic better than I do) can critique where you went wrong. I think (but don't know for sure) the problem is you won't be able to swap out the variables. We could try to say "it is true when we set $x=y$ and $y=x$ but that is actually meaningless. If $x$ and $y$ are set then $x\ne y$. We have to somehow "unset" a variable and reset it. I think..... – fleablood Sep 15 '18 at 16:02
• @fleablood: my reading of the rule spec is that it can't be applied in the case in question: the side-condition "$P$ admits $t$ for $v$" prevents the rule being applied. – Rob Arthan Sep 15 '18 at 20:08

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.
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)$.