The code I gave translates easily into Agda, a computerized proof checker, and as such more formal than most mathematics. However, here's the same thing in a mo

The code I gave translates easily into Agda, a computerized proof checker, and as such more formal than most mathematics. However, here's the same thing in a modernized version of Peano arithmetic. We assume all the usual properties of equality: reflexivity, symmetry, transitivity, and substitution. -- Axioms (only 1 and 2 are relevant) 1. 0 ∈ N 2. ∀ x∈N. S(x) ∈ N 3. ∀ x∈N. 0 ≠ S(x) 4. ∀ x∈N, y∈N. S(x) = S(y) ⊃ x = y 5. P(0) ∧ (∀ x∈N. P(x) ⊃ P(S(x))) ⊃ ∀ x∈N. P(x) -- Definition of addition 6. ∀ a∈N. a + 0 = a 7. ∀ a,b ∈ N. a + S(b) = S(a+b) -- Proof that S(0) + S(0) = S(S(0)) 9. S(0) ∈ N [from 2 and 1] 10. S(0) + S(0) = S(S(0) + 0) [from 7 and 9] 11. S(0) + 0 = S(0) [from 6 and 9] 12. S(S(0) + 0) = S(S(0)) [substitution of equals, from 11] 13. S(0) + S(0) = S(S(0)) [transitivity from 10 and 12] Edit: Ah, I see I was beaten to it by pavelrub.