¿Cuál fue la intención original para la creación del cálculo Lambda?

He leído que inicialmente Church propuso el cálculo como parte de su artículo Postulados de lógica (que es una lectura densa). Pero Kleene demostró que su "sistema" era inconsistente, después de lo cual Church extrajo cosas relevantes para su trabajo sobre "computabilidad efectiva" y abandonó su trabajo previo sobre lógica.$\lambda$

Entonces, según tengo entendido, el sistema y sus anotaciones tomaron forma como parte de algo relacionado con la lógica. ¿Qué estaba tratando de lograr inicialmente Church de lo que se bifurcó después? ¿Cuáles fueron las razones iniciales para crear -calculus?$\lambda$$\lambda$

Quería crear un sistema formal para los fundamentos de la lógica y las matemáticas que fuera más simple que la teoría de tipos de Russell y la teoría de conjuntos de Zermelo.

La idea básica era agregar una constante al cálculo lambda sin tipo (o lógica combinatoria) e interpretar X Z como expresión " Z satisface el predicado X " y Ξ X Y como expresión " X ⊆ Y ". Con reglas que expresan estas intenciones, uno puede interpretar el → $\Xi$$XZ$$Z$$X$$\Xi XY$$X\subseteq Y$${\to}{\forall}$ fragmento de la lógica de predicados intuicionistas y la comprensión sin restricciones, el único problema es que, según la paradoja de Curry, cada es derivable.$X$

Ver p. 7 de:

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

Además de la introducción a:

Barendregt, Bunder y Dekkers, Sistemas de lógica combinatoria illativa completa para cálculo proposicional y predicado de primer orden , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

No estoy seguro de si esto fue parte de la motivación para crear el cálculo lambda, pero el cálculo lambda se utilizó para resolver el problema Entscheidungs , planteado por Hilbert en 1928. Turing resolvió independientemente el problema Entscheidungs ​​introduciendo la máquina Turing.

Del artículo de Wikipedia sobre Entscheidungsproblem:

En 1936, Alonzo Church y Alan Turing publicaron documentos independientes [2] que muestran que una solución general al problema de Entscheidungs ​​es imposible, suponiendo que la noción intuitiva de "efectivamente calculable" es capturada por las funciones computables por una máquina de Turing (o equivalentemente, por los expresables en el cálculo lambda).