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$
5
  • $\begingroup$ Hint: prove $u+a=u+b\implies a=b$ by induction on $u$. $\endgroup$
    – Berci
    Commented Mar 31, 2019 at 23:28
  • $\begingroup$ If im able to prove that, how would I apply it to my proof? $\endgroup$
    – Thomas Formal
    Commented Mar 31, 2019 at 23:32
  • $\begingroup$ Oh I understand, could you give a hint on how to prove the statement you stated? $\endgroup$
    – Thomas Formal
    Commented Mar 31, 2019 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
    Commented Apr 1, 2019 at 0:35
  • $\begingroup$ More specifically, you need $s(u+y) =s(u)+y$ for the induction step. $\endgroup$
    – Berci
    Commented Apr 1, 2019 at 0:37

1 Answer 1

Reset to default
1
$\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$
2
  • $\begingroup$ thanks!, this would just be induction on u right? Not a triple induction on a , b and u? $\endgroup$
    – Thomas Formal
    Commented Apr 1, 2019 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
    Commented Apr 1, 2019 at 2:10

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .