Qual foi a intenção original para a criação do cálculo Lambda?

Eu li que, inicialmente, Church propôs o cálcio como parte de seu artigo Postulados da Lógica (que é uma leitura densa). Mas Kleene provou seu "sistema" inconsistente, após o qual Church extraiu coisas relevantes por seu trabalho sobre "computabilidade efetiva" e abandonou seu trabalho anterior sobre lógica.$\lambda$

Pelo que entendi, o sistema e suas notações tomaram forma como parte de algo a ver com lógica. O que Church estava inicialmente tentando alcançar, do qual ele se retirou mais tarde? Quais foram as razões iniciais para criar o λ- calcculus?$\lambda$$\lambda$

Ele queria criar um sistema formal para os fundamentos da lógica e da matemática que fosse mais simples que a teoria dos tipos de Russell e a teoria dos conjuntos de Zermelo.

A idéia básica era adicionar uma constante ao cálculo lambda não tipado (ou lógica combinatória) e interpretar X Z como expressão " Z satisfaz o predicado X " e Ξ X Y como expressão " X ⊆ Y ". Com regras expressar estas intenções pode-se então interpretar a → ∀ -fragment da lógica de predicados intuitionistic e compreensão irrestrita, o único problema é que, ao paradoxo de Curry, cada X é derivável.$\Xi$$XZ$$Z$$X$$\Xi XY$$X\subseteq Y$${\to}{\forall}$$X$

Veja a pág. 7 de:

Cardone e Hindley, História do cálculo lambda e lógica combinatória , 2006: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf

Bem como a introdução a:

Barendregt, Bunder e Dekkers, sistemas de lógica combinatória ilativa completos para cálculo proposicional e de predicados de primeira ordem , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

Não tenho certeza se isso fazia parte da motivação para criar o cálculo lambda, mas o cálculo lambda foi usado para resolver o problema de Entscheidung , apresentado por Hilbert em 1928. Turing resolveu independentemente o problema de Entscheidung introduzindo a máquina de Turing.

Do artigo da Wikipedia sobre Entscheidungsproblem:

Em 1936, Alonzo Church e Alan Turing publicaram artigos independentes [2], mostrando que uma solução geral para o problema de Entscheidung é impossível, assumindo que a noção intuitiva de "efetivamente calculável" seja capturada pelas funções computáveis ​​por uma máquina de Turing (ou equivalente, por aqueles expressáveis ​​no cálculo lambda).