Hacker News Reader

Comment by rntz | Hacker News Reader

Here is a simple definition of the natural numbers and addition, in Haskell:

    data Nat = Zero | Suc Nat

    plus :: (Nat, Nat) -> Nat
    plus (Zero, y) = y                  -- axiom 1
    plus (Suc x, y) = Suc (plus (x, y)) -- axiom 2

    one = Suc Zero
    two = Suc one

Here is a proof that plus (one, one) = two:

    plus (Suc Zero, Suc Zero)
    = Suc (plus (Zero, Suc Zero))  [by axiom 2]
    = Suc (Suc Zero)               [by axiom 1]

View on HN

Can you please translate that to mathematics? My request was regarding a formal mathematical proof.

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.

Reply on news.ycombinator.com