# Math Help - sucessor addition pf

prove that for all natural numbers x and y, S(x+y)=S(x)+y

Is this not strictly by definition of addition????

2. Yes, this is an interesting question. This totally depends on the context. This is one of the Peano's axioms for arithmetic, so in that context it is trivially derivable (provable). In other formalisms, there is a convention that the terms (S x) + y and S(x + y) are in fact the same term. (For example, this is the case in the Calculus of Inductive Constructions, the theory behind the Coq proof assistant.) In such systems, terms are not just strings of characters but equivalence classes of such strings. But in both of these cases one can say that this holds by definition.

Maybe it's a trivial part of a warm-up for further questions? Its purpose may be for readers to nod their heads, acknowledge that this is true and be ready to refer to this fact in more complicated discussions.