Most likely this subject has been covered many times here, still I fail to grasp this.
I can't understand how do we know that the successor of $1$ is $2$ based on Peano's axioms, given that we start from $1$ (for convenience, since the book I am reading starts from $1$)? It is all good to the point where we demonstrate that there is a unique function such that
- $f(x, 1) = x'$
- $f(x, y') = (f(x, y))'$
However, it all falls apart for me, when somehow magically $f(x, y')$ becomes $x+y'$ or particularly $f(x, 1) = x+1$, hence $x+1 = x'$. My problem is that, as we have never been told by axioms what successors really are, just defining the function $f$ through some plus-sign notation doesn't make it clear how to perform (calculate, evaluate) that operation. In my eyes, it is the same as if it was written like $f(x, 1) = x ? 1 = x'$ (yes, the operation is a question mark). So, how does $x ? 1$ imply that the successor of $1$ should be $2$? Where does it come from that we assign $2$ to the successor of $1$, $3$ to the successor of $2$, etc. besides the intuition that it should be this way?
P.S. It reminds me of a square root function $r(x)=\sqrt{x}$ with fancy notation $\sqrt{x}$, definition of which doesn't really tell us how to calculate one but rather defines a property of the result that whatever it is, its square should be equal to the $x$. Similar feeling about $x+1$ is also present here:
- either I have to know where it comes from that the successor of $1$ is $2$, then $x+1$ becomes a mere conventional notation for the successor, on top of which more general operation $x+y$ is defined
- or how to actually perform $x+1$ to get $2$, when $x=1$, which is not obvious to me from the axioms. Although I have an intuition how to define $x+1$ through set-theoretic notation, where natural numbers are defined through empty set ($0 = \varnothing,1 = \{\varnothing, \{\varnothing\}\}, \dots$), I am interested how it derives from Peano's axioms, not from the set theory.