I'm doing my research project on Peano Arithmetic, and need to show the PA can prove that no number is the successor of itself.
I've seen an answer here: Peano's Axiom: Is it implied that successor of a number is not the number itself?, but I'm struggling to understand from line 5 - why is it introduced? And why is line 6 introduced?
Thanks in advance for your help
Dani
In order to answer that, it must be seen what lines # and fou say.
Line 3: If $s(0)\neq0$ and if, for every natural $n$, $s(n)\neq n\implies s\bigl(s(n)\bigr)\neq s(n)$, then, for every $n$, $s(n)\neq n$.
This is just the induction principle applied to the proposition $(\forall n\in\mathbb{N}):s(n)\neq n$.
Line 4: $s(0)\neq 0$
This is here to assert that the base case of induction holds.
Then lines 5 to 10 are here to prove that if $s(n)\neq n$, then $s\bigl(s(n)\bigr)\neq s(n)$, that is, in order to comple that induction proof. So, he starts by picking an $a\in\mathbb N$ and he assumes that $s(a)\neq a$. In order to prove that $s\bigl(s(a)\bigr)\neq s(a)$, he assumes that they are equal and reaches a contradiction. Since such a contradiction is reached, $s\bigl(s(a)\bigr)$ is indeed different form $s(a)$ and the theorem is proved.