Check out the axioms of Peano Arithmetic: http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic If we use D

Check out the axioms of Peano Arithmetic: http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic http://en.wikipedia.org/wiki/Peano_axioms#Arithmetic If we use Dedekind's recursive definition of addition, and the definitions 1=S(0) and 2=S(S(0)), then: S(0) + S(0) = S(S(0)+0) = S(S(0)) I know the computer proof assistant Isabelle/HOL, inspired by the Principia Mathematica, can prove simple theorems about arithmetic using a "rewrite" system similar to what I've done above.