> The actual details of how to implement zero and successor should be implemented as are left as someone else’s problem — we can survive without them. All we ca

> The actual details of how to implement zero and successor should be implemented as are left as someone else’s problem — we can survive without them. All we care about is that our numbers do the right thing, given whatever zero and successor someone may provide. Zero is left as an implementation detail (it can actually be quite literally anything -- as long as it's not the successor). One is simply the successor function applied to zero. From http://www.cs.unc.edu/~stotts/723/Lambda/church.html http://www.cs.unc.edu/~stotts/723/Lambda/church.html -- Natural numbers are non-negative. Given a successor function, next, which adds one, we can define the natural numbers in terms of zero and next: 1 = (next 0) 2 = (next 1) = (next (next 0)) 3 = (next 2) = (next (next (next 0))) and so on. Therefore a number n will be that number of successors of zero. Just as we adopted the convention TRUE = first, and FALSE = second, we adopt the following convention: zero = Lf.Lx.x one = Lf.Lx.(f x) two = Lf.Lx.(f (f x)) three = Lf.Lx.(f (f (f x))) four = Lf.Lx.(f (f (f (f x))))