Exploring the Peano Axioms Through Algebraic Data Types | Hacker News Reader

Exploring the Peano Axioms Through Algebraic Data Types

francisrstokes.github.io

Strictly speaking, aren’t these the axioms of Robinson arithmetic (a much weaker system)? For Peano arithmetic you need the axiom schema of induction as well.

I think structural induction over S will do just fine.

I thought that the recursively enumerable structure was given by the Axiom of Induction.

I don't understand how .add as defined could terminate.

Base case is 0 add y = 0

Recursion is Sx add y = Sy add x

Which is of course _swap_

Shouldn't it be = S (x add y)

Let's try it with x = 2, y = 5:

    S(2) add 5       (i.e. 3 + 5)
     => 2 add S(5)   (i.e. 2 + 6)
     => S(1) add 6   (i.e. 2 + 6)
     => 1 add S(6)   (i.e. 1 + 7)
     => S(0) add 7   (i.e. 1 + 7)
     => 0 add S(7)   (i.e. 0 + 8)
     => 0 add 8
     => 8            (base case)

I agree that your rule would work too though:

    S(2) add 5
     => S(1 add 5)
     => S(S(0 add 5))

Seems more sensible to me, and by adding the same rule to the right hand side we end up only needing a single base case (that 0+0=0)

     => S(S(S(0 add 4)))
    ...
     => S(S(S(S(S(S(S(S(0 add 0))))))))
     => S(S(S(S(S(S(S(S(0))))))))
         = 8 (that is the definition of 8)

You swapped the order of method arguments though

you are doing x add Sy which isn't the same as Sy add x

        Number.prototype.add = function (y) {
          var x = Number(this)
          return x===0 ? y : (y+1).add(x-1)
        }

        console.log(Number(3).add(2)) // infinite

Oops, sorry, I see what you mean now. You're right, it looks like this is a mistake:

    S: innerX => S(y).add(innerX)

It should be

    S: innerX => S(innerX).add(y)

The recursion is S(x) add y => x add S(y), which recurses until the x becomes O() so it hits the base case.

Would have been cool to show it in Coq as well, to make the connection to formal mathematics more clear!

Reply on news.ycombinator.com