Yes I am in agreement with you about the labels. But, I am not convinced that Peano wrote that stuff without already having been biased by the notion of the number line. Also, given * 1 is a natural number * For all x, Sx is a natural number * For all x, Sx is not 1 * For all x and y, x = y iff Sx = Sy I still maintain the early phrase "For all x" is unfortunate. It clearly can be interpreted as saying "for all the x that already exist." This is very much a problem in my opinion. It feels as if the system is riding on the edge of chicken and egg. I am sorry but it will take me some time to absorb that it is not a chicken and egg system (I will take the mathematicians word for it for now). If, however, the numbers can exist without the successor function definition (example: in terms of counting only and not in terms of talking about where the counting stops) then clearly there is a problem with the definition of Prime. It refers not to the "position" where the counting stops UNTIL the operational axioms are applied.