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.