22
$\begingroup$

I've read that initially Church proposed the $\lambda$-calculus as part of his Postulates of Logic paper (which is a dense read). But Kleene proved his "system" inconsistent after which, Church extracted relevant things for his work on "effective computability" and abandoned his prior work on logic.

So as I understand it, the $\lambda$-system and its notations took form as part of something to do with logic. What was Church initially trying to achieve that he forked off from later? What were the initial reasons for creating $\lambda$-calculus?

$\endgroup$
  • 1
    $\begingroup$ Typo in the title... $\endgroup$ – user11153 Feb 13 '15 at 11:09
26
$\begingroup$

He wanted to create a formal system for the foundations of logic and mathematics that was simpler than Russell's type theory and Zermelo's set theory.

The basic idea was to add a constant $\Xi$ to the untyped lambda calculus (or combinatory logic) and interpret $XZ$ as expressing "$Z$ satisfies the predicate $X$" and $\Xi XY$ as expressing "$X\subseteq Y$". With rules expressing these intentions one can then interpret the ${\to}{\forall}$-fragment of intuitionistic predicate logic and unrestricted comprehension, the only problem being that by Curry's paradox, every $X$ is derivable.

See p. 7 of:

Cardone and Hindley, History of Lambda-calculus and Combinatory Logic, 2006: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf

As well as the introduction to:

Barendregt, Bunder and Dekkers, Systems of Illative Combinatory Logic Complete for First-Order Propositional and Predicate Calculus, JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

$\endgroup$
  • 8
    $\begingroup$ "The only problem being that by Curry's paradox, every $X$ is derivable" :) It might be useful to remind what curry's paradox is: Given that there exists a term $Y$ such that $YM=M(YM)$ for every $M$, one can then write $Y(\neg)$ which is a proposition $\phi$ such that $\phi\Leftrightarrow\neg\phi$, giving the same contradiction as for Russel's paradox. Non-termination is crucial here, which motivated the creation of simply typed $\lambda$-calculus, in which every term terminates. $\endgroup$ – cody Feb 13 '15 at 19:07
2
$\begingroup$

I'm not sure if this was part of the motivation for creating the lambda calculus, but the lambda calculus was used to resolve the Entscheidungsproblem, posed by Hilbert in 1928. Turing independently resolved the Entscheidungsproblem by introducing the Turing machine.

From the Wikipedia article on Entscheidungsproblem:

In 1936, Alonzo Church and Alan Turing published independent papers[2] showing that a general solution to the Entscheidungsproblem is impossible, assuming that the intuitive notion of "effectively calculable" is captured by the functions computable by a Turing machine (or equivalently, by those expressible in the lambda calculus).

$\endgroup$
  • 1
    $\begingroup$ That's the "aftermath" of having created Lambda calculus earlier. He just reused a critical part of it for providing a definition for effective calculability. $\endgroup$ – PhD Feb 13 '15 at 21:30

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.