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...

▲

rtpg a day ago | parent [-]

Yeah I've been meaning to send a request to Princeton's libraries with his notes but don't know what a good request looks like

The jump from "there is a successor operator" to "numbers take a successor operator" is interesting to me. I wonder if it was the first computer science-y "oh I can use this single thing for two things" moment! Obviously not the first in all of science/math/whatever but it's a very good idea

	▲	black_knight a day ago \| parent \| next [-]
		The idea of Church numerals is quite similar to induction. An induction proof extends a method of treating the zero case and the successor case, to a treatment of all naturals. Or one can see it as defining the naturals as the numbers reachable by this process. The leap to Church numerals is not too big from this.
	▲	measurablefunc a day ago \| parent \| prev [-]
		Probably not possible unless you have academic credentials to back up your request like being a historian writing a book on the history of logic & computability.