2
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Seems related to this question of mine: math.stackexchange.com/questions/476184/… $\endgroup$ – marty cohen Aug 4 '17 at 19:50
  • 1
    $\begingroup$ 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. $\endgroup$ – Peyton Aug 4 '17 at 19:52
  • $\begingroup$ Indeed @martycohen, but I was interested in the solution using Peano arithmetic axioms $\endgroup$ – Akuri Aug 5 '17 at 3:27
1
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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)$ $\endgroup$ – Hagen von Eitzen Aug 4 '17 at 20:47
  • $\begingroup$ I think you also need $\forall x,y \in \mathbb{N}:x+y \in \mathbb{N}$ which is another induction $\endgroup$ – Akuri Aug 5 '17 at 2:34
  • $\begingroup$ Ok, I mechanized it. It also required associativity and commutativity. Thanks. $\endgroup$ – Akuri Aug 5 '17 at 3:23
  • 1
    $\begingroup$ @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. $\endgroup$ – Bram28 Aug 5 '17 at 12:57
  • $\begingroup$ Some typo there, it's $\forall x~s(x)+s(x)=s(x+s(x))$, right? $\endgroup$ – Akuri Aug 5 '17 at 18:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.