# Proof of $\forall x \forall y(x+x \neq y+y+1)$ in Peano arithmetic

How to prove $\forall x \forall y(x+x \neq y+y+1)$ using the axioms of Peano arithmetic?

• Seems related to this question of mine: math.stackexchange.com/questions/476184/… – marty cohen Aug 4 '17 at 19:50
• For all $y$, $0\neq y+y+1= S(y+y)$ because $0$ is not a successor. Assume $x+x\neq y+y+1$ for all $y$. Then $x+x+1+1\neq y+y+1+1+1$ for all $y$. This means that $(x+1)+(x+1)\neq y+ y+ 1$ for all $y\neq0$. But also $(x+1)+(x+1)\neq 0+0+1$ because otherwise $x+x+1=0$ and $0$ is not a successor. Therefore, by induction on $x$ we get the proposition. – Peyton Aug 4 '17 at 19:52
• Indeed @martycohen, but I was interested in the solution using Peano arithmetic axioms – Akuri Aug 5 '17 at 3:27

We take $\Bbb{N}$ to include zero.

For $x\in \Bbb N$ let proposition $P_x$ be $$\forall y\in \Bbb N (x+x \neq y+y+1)$$ Let $K$ be the set of all $x$ such that $P_x$ is true. We will establish induction on $K$, to show that $K$ contains every natural number.

To show that zero is in $K$ we must prove $$\forall y \in \Bbb N ( 0+0 \neq y+y+1)$$ But by the additive identity property, $u+0 = u$ and in particular $0+0 = 0$. And (with $S(t)$ the successor function), by the definition of $1$ $v+1 = v+S(0)$. Substituting $(y+y)$ for $v$ that reads $$(y+y)+1 = S(y+y)$$ And by the first ordering axiom, $0$ is not the successor of any natural number, so $0 \neq (y+y)+1$ so $$\forall y\in \Bbb N ( 0+0 \neq y+y+1)$$

To complete the conditions of the axiom of induction we must show that for every natural number $n$, $n\in K \implies S(n) \in K$.

By the induction hypothesis $P_n$ is true. So $$\forall y\in \Bbb N ( n+n \neq y+y+1)$$ Now assume that for some $y \in \Bbb N$ it were true that $(n+1)+(n+1) = y+y+1$. By the commutative and associative properties of additions, that would be the same as $$(n+n+1) + 1 = y+y+1 \\ S(n+n+1) =S(y+y)$$ and by the second axiom defining the successor function if $S(n+n+1)=S(y+y)$ then $$y+y=n+n+1$$ That forces $y \neq 0$ by the same "$0$ is not a successor" argument, and also says $y+y = S(n+n)$. Now it is easy to show (again using induction) that $\forall p\in \Bbb N^+( \exists q : (p=S(q))$ so in particular $\exists z : y=S(z)$.

Then $$y+y = S(z) + S(z) = (z+1)+(z+1) = (z+z+1)+1 = S(z+z+1) y+y = n+n+1 \implies S(z+z+1) = n+n+1 = S(n+n) \implies (z+z+1) =(n+n)$$ which contradicts the induction hypothesis.

So for all $y\in \Bbb N$ we have shown that $(n+1)+(n+1) \neq y+y+1$. But replacing $x$ by $(n+1)$ in the definition of $K_x$, this is just the statement of $K_{n+1}$: $$\forall y\in \Bbb N ( (n+1)+(n+1) \neq y+y+1$$ Thus induction is established, $K$ includes all natural numbers, $P_x$ is true whenever $x$ is a natural number, and the theorem is proven.

• Just an idea: It might simplify the argument if we let $P_x$ be the stronger $\forall y(x+x\ne y+y+1\land y+y\ne x+x+1)$ – Hagen von Eitzen Aug 4 '17 at 20:47
• I think you also need $\forall x,y \in \mathbb{N}:x+y \in \mathbb{N}$ which is another induction – Akuri Aug 5 '17 at 2:34
• Ok, I mechanized it. It also required associativity and commutativity. Thanks. – Akuri Aug 5 '17 at 3:23
• @Akuri You can do it without commutation and association. Just use induction to prove $\forall x \forall y \ s(x) + y = s(x + y)$, and use that and PA4 to prove $\forall x \ s(x) + s(x) = s(s(x))$. With that and $\forall x \ x + s(0) = s(x)$ as two Lemma's you can now prove your result using induction quite easily and without Commutation and Association. – Bram28 Aug 5 '17 at 12:57
• Some typo there, it's $\forall x~s(x)+s(x)=s(x+s(x))$, right? – Akuri Aug 5 '17 at 18:19