That makes sense, thank you. However, at what point is the symbol "2" introduced in such a scheme? Is it before addition, or after? At some point it is given a definition, like S(S(0)) where S(0)=1 and S(X)=X+1, at which point isnt it easy to substitute

  2 = S(S(0))= S(0)+1 = 1+1

is this simple equivalence really not provable with sufficient axioms?

Obviously from the downvotes I am missing something fundamental, I would very much like to know what that is but am at a loss. Perhaps I am just missing mrleiter's original point.