Lambda the Ultimate

Church's λ-calculus was a restriction of his 1932/3 logic, which he'd been developing through the 1920s (I don't recall off hand just when he started it). The 1932 publication of that logic billed it as an effort to avoid paradoxes by a different means than the usual dropping of the Law of the Excluded Middle — very much in keeping with David Hilbert's thinking on the matter, not only in taking a formalist approach to setting up the logic (Church suggested in the 1932 paper that if the formal system wasn't useful as a logic it might still be useful for some other purpose), but also in that Hilbert maintained the Excluded Middle was too useful to give up without a fight, his formalist program being the means by which he proposed to investigate what could be done short of dropping the Excluded Middle. Church proposed to keep a slightly-modified form of the Excluded Middle, and weaken reductio ad absurdum. At the same time, the 1932 paper starts with only a brief mention of that paradox-avoidance strategy before launching into a rant against the evils of uncertainty over the meaning of variables, for which Church's solution was to have all variables bound by a single simple binding device called λ, which could be made to do for everything by the (imho quite lovely) device of using higher-order function primitives for universal and existential quantification. (The idea here was that (Σ F) means there exists X such that (F X) is true, while (Π F) means for all X, (F X) is true.) I've become aware in the past three years or so that the formalist origin of this single-binding-device strategy has had a profound effect on how mathematicians conceptualize term-calculus variables.

Meanwhile, back on the paradox-avoidance track, by 1935 Church's team (Kleene and Rosser) had published a proof that Church's logic supported a form of the Richard paradox, and a natural next step after that was to back off from the full logic and look for a subset that could be proven consistent. A general notion of consistency, for systems that don't necessarily have negation, is that not all propositions are equivalent to each other; and if you back off from Church's full logic by removing all the logical operators, leaving only λ, it's possible to prove that not all terms are equivalent to each other. This theorem, published in 1936, is what's now called the Church-Rosser Theorem. That subset of the logic is, of course, λ-calculus.