In April 1936 the American logician Alonzo Church published “An Unsolvable Problem of Elementary Number Theory” in the American Journal of Mathematics, volume 58, number 2, pages 345 to 363. The source cited here is a scan of the original journal article carrying the standard JSTOR cover page that records its full bibliographic details. The paper is one of the two founding results of computability theory, the other being Alan Turing’s paper of the same year.
Church’s tool was the lambda calculus, a compact formal system he had developed for describing functions purely in terms of how they take inputs and produce outputs, using nothing but variables, function definition, and application. In this paper he proposed that the intuitive notion of a function being “effectively calculable,” that is, computable by a finite mechanical procedure, could be identified with being definable in the lambda calculus, an idea that is one half of what later became known as the Church-Turing thesis. He then proved that there is a precisely stated problem about whole numbers for which no such procedure can exist. No effective method can decide it in every case.
This unsolvability result is closely related to Godel’s incompleteness theorems of 1931 and to Hilbert’s decision problem, the Entscheidungsproblem. Where Godel showed that formal systems cannot prove every truth, Church showed that there is no mechanical procedure to decide every question, attacking the problem through a definition of computation rather than through provability. Turing reached the same conclusion at almost the same time using his abstract machines, and the two definitions were soon proved to pick out exactly the same class of computable functions.
The lambda calculus did not stay a tool for proving impossibility results. Because it is a complete and elegant model of computation built entirely from functions, it became one of the deep roots of computer science. It directly shaped the design of functional programming and of John McCarthy’s Lisp, and it remains a foundation for how programming languages are defined and reasoned about today.