The calculi of lambda-conversion. (English) JFM 67.0041.01

Church, A.

(Annals of mathematics studies, No. 6.) 77 S. Princeton, Princeton University Press (1941).

Man denke sich einen Kalkül, so daß \(M\) in bezug auf diesen Kalkül ein sinnvoller Ausdruck ist. \(x\) komme in \(M\) frei vor. In diesen Kalkül sei das \(\lambda \)-Symbol so eingeführt, daß \(\lambda xM\) interpretiert werden kann als die Funktion, deren Funktionswert für jedes zur Konkurrenz zugelassene Argument \(\alpha \) die Bedeutung des Ausdrucks ist, den man aus \(M\) dadurch erhält, daß \(x\) an jeder Stelle, an der \(x\) in \(M\) frei vorkommt, durch ein und dasselbe \(\alpha \)-Symbol ersetzt wird. Dann hat man die Basis des Lambda-Kalküls.
Der Weg von dieser Basis bis zur Konstituierung eines (ein möglichst großes Segment der Mathematik umfassenden) Logikkalküls, für den die Widerspruchsfreiheit bewiesen werden kann, ist so weit, so abstrakt und so ungewöhnlich, daß er hier nicht angedeutet werden kann. Der erzielte Kalkül trägt finitistische Züge. Die Alternative von \(A\) und \(B\) ist beweisbar in ihm dann und nur dann, wenn \(A\) beweisbar oder \(B\) beweisbar ist. Die Ausdrucksmittel und -möglichkeiten, insbesondere in bezug auf die Generalisierung, reichen an die der Principia Mathematica nicht heran.
Es scheint mir, daß das Interesse an diesem Kalkül auf die folgenden drei Hauptpunkte konzentriert werden darf: (1) Dieser Kalkül ist typenfrei. Hierauf wird zwar nirgends Bezug genommen. Es scheint mir jedoch, daß das Desiderat eines im mathematischen Sinne möglichst ausdrucksvollen typenfreien Logikkalküls, für den die Widerspruchsfreiheit bewiesen werden kann, das Hauptmotiv dieser Kalkülschöpfung gewesen ist. – (2) Für diesen Kalkül kann die Widerspruchsfreiheit mit den Beweismitteln einer im strengen Sinne finitistisch-konstruktiven Metalogik bewiesen werden. – (3) Das \(\lambda \)-Symbol ist in diesen Kalkül so eingeführt, daß mit Hilfe dieses Symbols nicht nur die Gödelschen Zahlen formalisiert werden können, sondern auch ein für metamathematische Untersuchungen so wichtiger Begriff wie der der effektiv berechenbaren Funktion, dessen erste Präzisierung dem Verf. zu verdanken ist. – In das Konstituierungsverfahren gehen außer den grundlegenden Begriffen der Lambda-conversion und Lambda-definability noch die Prozesse der \(\lambda \)-\(\varkappa \)-Konversion und \(\lambda \)-\(\delta \)-Konversion ein. An dem Aufbau und der Diskussion dieses Kalküls sind neben dem Verf. Kleene und Rosser besonders beteiligt gewesen. Die vorliegende Skizze besteht aus fünf Kapiteln mit folgenden Stichworten: I. Introductory; II. Lambda-Conversion; III. Lambda-Definability (1. Lambda-definability of functions of positive integers, 2. Ordered pairs and triads, the predecessor-function, 3. Propositional functions, the Kleene \(p\)-function, 4. Definition by recursion); IV. Combinations, Gödel numbers; V. The calculi of \(\lambda \)-\(\varkappa \)-conversion and \(\lambda \)-\(\delta \)-conversion (1. The calculus of \(\lambda \)-\(\varkappa \)-conversion, 2. The calculus of restricted \(\lambda \)-\(\varkappa \)-conversion, 3. Transfinite ordinals, 4. The calculus of \(\lambda \)-\(\delta \)-conversion, 5. A system of symbolic logic).

Reviewer: Scholz, Heinrich, Prof. (Münster), [ZBL]

JFM Section:

Erster Halbband. B. Grundlagen der Mathematik. Logik. b) Grundlagenforschung. Logik.