Apa maksud awal dari pembuatan kalkulus Lambda?

Saya pernah membaca bahwa pada awalnya Gereja mengusulkan -calculus sebagai bagian dari postulat makalah Logic-nya (yang merupakan bacaan padat). Tetapi Kleene membuktikan "sistem" -nya tidak konsisten setelah itu, Gereja mengekstraksi hal-hal yang relevan untuk karyanya tentang "komputabilitas yang efektif" dan mengabaikan karyanya yang sebelumnya tentang logika.$\lambda$

Jadi seperti yang saya pahami, sistem dan notasinya mengambil bentuk sebagai bagian dari sesuatu yang berkaitan dengan logika. Apa yang awalnya Gereja coba capai yang dia potong kemudian? Apa alasan awal untuk membuat -calculus?$\lambda$$\lambda$

Dia ingin membuat sistem formal untuk fondasi logika dan matematika yang lebih sederhana daripada teori tipe Russell dan teori himpunan Zermelo.

Ide dasarnya adalah untuk menambahkan konstanta ke kalkulus lambda yang tidak diketik (atau logika kombinasi) dan menafsirkan X Z sebagai menyatakan " Z memenuhi predikat X " dan Ξ X Y sebagai menyatakan " X ⊆ Y ". Dengan aturan yang menyatakan niat ini maka seseorang dapat menafsirkan → ∀ -fragment dari logika predikat intuitionistic dan pemahaman tidak terbatas, satu-satunya masalah adalah bahwa dengan paradoks Curry, setiap X dapat diturunkan.$\Xi$$XZ$$Z$$X$$\Xi XY$$X\subseteq Y$${\to}{\forall}$$X$

Lihat hal. 7 dari:

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

Serta pengantar:

Barendregt, Bunder dan Dekkers, Sistem Logika Combinatory Illative Lengkap untuk Proposisional dan Predikat Kalkulus Orde Pertama , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

Saya tidak yakin apakah ini merupakan bagian dari motivasi untuk membuat kalkulus lambda, tetapi kalkulus lambda digunakan untuk menyelesaikan Entscheidungsproblem , yang diajukan oleh Hilbert pada tahun 1928. Turing secara mandiri menyelesaikan Entscheidungsproblem dengan memperkenalkan mesin Turing.

Dari artikel Wikipedia di Entscheidungsproblem:

Pada tahun 1936, Gereja Alonzo dan Alan Turing menerbitkan makalah independen [2] yang menunjukkan bahwa solusi umum untuk Entscheidungsproblem tidak mungkin, dengan asumsi bahwa gagasan intuitif "dihitung secara efektif" ditangkap oleh fungsi yang dapat dihitung oleh mesin Turing (atau setara, oleh yang dapat diungkapkan dalam kalkulus lambda).