4 ms·
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) =
by rntz 13y ago
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]
- a1a 13y agoCan you please translate that to mathematics? My request was regarding a formal mathematical proof.
- rntz 13y agoThe 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.