0
$\begingroup$

I'm trying to prove:

$\forall x\forall y((x=y)\longrightarrow(x\not<y)$

I tried starting off with

$u=v, u+s(z) = v\vdash u = v$

$u=v, u+s(z) = v\vdash u+s(z) = v$

. . .

$u=v, u+s(z) = v\vdash s(z) = 0$

and try to get a contradiction (since $s(z) \not = 0$, is a theorem), but I'm having a lot of difficulty proving that $s(z) = 0$.

Any help would be greatly appreciated.

$\endgroup$
  • $\begingroup$ Hint: prove $u+a=u+b\implies a=b$ by induction on $u$. $\endgroup$ – Berci Mar 31 at 23:28
  • $\begingroup$ If im able to prove that, how would I apply it to my proof? $\endgroup$ – Thomas Formal Mar 31 at 23:32
  • $\begingroup$ Oh I understand, could you give a hint on how to prove the statement you stated? $\endgroup$ – Thomas Formal Mar 31 at 23:33
  • $\begingroup$ It can depend on the exact forms of the Peano axioms you're using, and/or basic statements that are already proved, e.g. commutativity of addition. $\endgroup$ – Berci Apr 1 at 0:35
  • $\begingroup$ More specifically, you need $s(u+y) =s(u)+y$ for the induction step. $\endgroup$ – Berci Apr 1 at 0:37
0
$\begingroup$

Use the following lemma: $$\forall a,b,u:\, u+a=u+b\to a=b$$ This can be proved by induction on $u$, provided we already know $s(x+y)=s(x)+y\,$ (which is another lemma if the axiom is stated in the other argument).

The base case $u=0$ is immediate.
Now suppose $s(u)+a=s(u)+b$. Then using the above statement, we have $s(u+a)=s(u+b)$. Then injectivity of $s$ implies $u+a=u+b$ which implies $a=b$ by induction hypothesis.

$\endgroup$
  • $\begingroup$ thanks!, this would just be induction on u right? Not a triple induction on a , b and u? $\endgroup$ – Thomas Formal Apr 1 at 2:08
  • $\begingroup$ I was able to prove this result, but our version of the lemma was $x+s(y) = s(x + y)$, would proving the one you wrote require induction again? $\endgroup$ – Thomas Formal Apr 1 at 2:10

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.