I have myself usually seen Peano arithmetic described with 0 and the successor operation (such as in the context of actually implementing it in a computer). in this case,
where the two theorems needed are that x + S(y) = S(x) + y and that x + 0 = x. I find this to have less incidental complexity (given that we are interested in working up from axioms, not down from conventional arithmetic) perhaps because the tree of the final expression has no branches. The first theorem can be looked at as expressing that “moving stuff results in the same stuff”, i.e. a conservation law; note that the expression has precisely the same number of nodes.
I have myself usually seen Peano arithmetic described with 0 and the successor operation (such as in the context of actually implementing it in a computer). in this case,
where the two theorems needed are that x + S(y) = S(x) + y and that x + 0 = x. I find this to have less incidental complexity (given that we are interested in working up from axioms, not down from conventional arithmetic) perhaps because the tree of the final expression has no branches. The first theorem can be looked at as expressing that “moving stuff results in the same stuff”, i.e. a conservation law; note that the expression has precisely the same number of nodes.