Каково было первоначальное намерение для создания лямбда-исчисления?

Я читал, что изначально Черч предложил -calculus как часть своей статьи «Постулаты логики» (которая читается плотно). Но Клини доказал свою «систему» ​​непоследовательной, после чего Черч извлек соответствующие вещи для своей работы по «эффективной вычислимости» и отказался от своей предыдущей работы над логикой.$\lambda$

Насколько я понимаю, -система и ее обозначения приняли форму как часть чего-то общего с логикой. Чего изначально пытался достичь Церковь, от чего он отказался позже? Каковы были первые причины создания -calculus?$\lambda$$\lambda$

Он хотел создать формальную систему для основ логики и математики, которая была бы проще, чем теория типов Рассела и теория множеств Цермело.

Основная идея состояла в том, чтобы добавить константу к нетипизированному лямбда-исчислению (или комбинаторной логике) и интерпретировать как выражение " удовлетворяет предикату ", а как выражение " ". С помощью правил, выражающих эти намерения, можно затем интерпретировать -фрагмент интуиционистской логики предикатов и неограниченного понимания, единственная проблема заключается в том, что, согласно парадоксу Карри, каждый выводим.$\Xi$$XZ$$Z$$X$$\Xi XY$$X\subseteq Y$${\to}{\forall}$$X$

Смотрите стр. 7 из:

Кардоне и Хиндли, История лямбда-исчисления и комбинаторной логики , 2006: http://www.users.waitrose.com/~hindley/SomePapers_PDFs/2006CarHin,HistlamRp.pdf

А также введение в:

Барендрегт, Бандер и Деккерс, Системы илляционной комбинаторной логики, полные для исчисления высказываний и предикатов первого порядка , JSL 58-3 (1993): http://ftp.cs.ru.nl/CompMath.Found/ICL1.ps

Я не уверен, было ли это частью мотивации для создания лямбда-исчисления, но лямбда-исчисление использовалось для решения проблемы Entscheidungs , поставленной Гильбертом в 1928 году. Тьюринг самостоятельно решил проблему Entscheidungs , представив машину Тьюринга.

Из статьи Википедии по проблеме Entscheidungs:

В 1936 году Алонзо Черч и Алан Тьюринг опубликовали независимые статьи [2], в которых показано, что общее решение проблемы Энтшайдунга невозможно, если предположить, что интуитивное понятие «эффективно вычисляемый» охватывается функциями, вычисляемыми машиной Тьюринга (или, что то же самое, выражаемые в лямбда-исчислении).