What was the original intent for the creation of Lambda calculus?

Question

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?

Answer 1

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

Answer 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, 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).