alt Hacker NewsVery interesting historical document, though I don't have that much confidence in the precision of the explanation of the terms.
Related to this: does anyone know if there's any document that delves into how Church landed on Church numerals in particular? I get how they work, etc, but at least the papers I saw from him seem to just drop the definition out of thin air.
Were church numerals capturing some canonical representation of naturals in logic that was just known in the domain at the time? Are there any notes or the like that provide more insight?
Replies
While I don't know much about Church numbers or the theory how lambda calculus works, taking a glance at the definitions on wikipedia they seem to be the math idea of how numbers works (at the meta level)
I forgot the name of this, but they seem the equivalent of successors in math In the low level math theory you represent numbers as sequences of successors from 0 (or 1 I forgot)
Basically you have one then sucessor of one which is two, sucessor of two and so on So a number n is n successor operations from one
To me it seems Church numbers replace this sucessor operation with a function but it's the same idea
Their structural properties are similar to Peano's definition in terms of 0 and successor operation. ChatGPT does a pretty good job of spelling out the formal structural connection¹ but I doubt anyone knows how exactly he came up with the definition other than Church.
¹https://chatgpt.com/share/693f575d-0824-8009-bdca-bf3440a195...
Before Church there was Peano, and before Peano there was Grassmann
> It is rather well-known, through Peano's own acknowledgement, that Peano […] made extensive use of Grassmann's work in his development of the axioms. It is not so well-known that Grassmann had essentially the characterization of the set of all integers, now customary in texts of modern algebra, that it forms an ordered integral domain in which each set of positive elements has a least member. […] [Grassmann's book] was probably the first serious and rather successful attempt to put numbers on a more or less axiomatic basis.