It's one of the possible definitions. You could as well define next(x) = min(y such as y>x) and define 2 as next(next(0)) (0 can be defined as either x such as for all y y+x = y, or as x such that for all y x<y, depending on what set you are working with). Proving that 2 is 1+1 would be a theorem then. Of course, that works only for integers :)