<p>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 <a href="http://en.wikipedia.org/wiki/Entscheidungsproblem" rel="nofollow">Entscheidungsproblem</a>, posed by Hilbert in 1928.  Turing independently resolved the Entscheidungsproblem by introducing the Turing machine.</p>

<p>From the Wikipedia article on Entscheidungsproblem:</p>

<blockquote>
  <p>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).</p>
</blockquote>

CC BY-SA 3.0
2015-02-13T21:30:29.213Z
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.
PhD
CC BY-SA 3.0
2015-02-13T09:12:09.047Z
2015-02-13T09:12:09.047Z
littleO
<p>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.</p>

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

<p>See p. 7 of:</p>

<p>Cardone and Hindley, <em>History of Lambda-calculus and Combinatory Logic</em>, 2006:
<a href="http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf">http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf</a></p>

<p>As well as the introduction to:</p>

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

CC BY-SA 3.0
2015-02-13T19:07:30.003Z
"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.
cody
CC BY-SA 3.0
2015-02-13T04:41:26.707Z
2015-02-13T04:41:26.707Z
Ulrik Buchholtz
<p>I've read that initially Church proposed the $\lambda$-calculus as part of his <em>Postulates of Logic</em> 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.</p>

<p>So as I understand it, the $\lambda$-system and its notations took form as part of <em>something</em> 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?</p>

<lo.logic><big-picture><lambda-calculus><ho.history-overview>
What was the original intent for the creation of Lambda calculus?
PhD
# What was the original intent for the creation of Lambda calculus?

(Asked by: username_0 on 2015-02-12)

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?

**Tags:** lo.logic, big-picture, lambda-calculus, ho.history-overview


---

## 2 answers

### Answer by username_2 on 2015-02-13. Score: 26 | Accepted answer

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>

> **Comments:**
> **username_3**: "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.  

---

### Answer by username_1 on 2015-02-13. Score: 2

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](http://en.wikipedia.org/wiki/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).

> **Comments:**
> **username_0**: 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.  

---

