Ein System der typenfreien Logik. I. (Q2579580)

Eines der bemerkenswertesten neueren Ereignisse im Bereich der formalisierten Logik ist die mit einer Abhandlung von W. V. Quine vom Jahre 1936 beginnende Folge von Formalisierungen der auf die Schöpfung von E. Zermelo oder ihre Modifizierung durch J. v. Neumann zurückgehenden sogenannten mengentheoretischen Logik (W. Ackermann, P. Bernays, T. Skolem). Vor dem Russellschen Stufenkalkül im Sinn der sogenannten vereinfachten Typentheorie haben diese mengentheorischen Logikkalküle zwei wesentliche Vorzüge voraus: (1) den Vorsprung einer bemerkenswerten formalisierungstechnischen Vereinfachung, (2) eine wesentliche und zugleich das inhaltliche mathematische Denken befriedigende Bereicherung der Ausdrucks- und der Beweismöglichkeiten. Gleichzeitig ist es gelungen (vgl. \textit{W. V. Quine}, Amer. math. Monthly 44 (1937), 70-80; JFM 63.0022.*), auf eine Art, die den bis jetzt bekannten Prüfungsmethoden standgehalten hat, den Russell-Kalkül auf eine fast typenfreie Basis zu stellen. Durch diese Konstruktion wird der Stufenkalkül in bezug auf seine Ausdrucks- und Beweismöglichkeiten an den mengentheoretischen Logikkalkül herangerückt. Diese Leistungen sind als wesentliche Fortschritte anzusehen. Aber auch sie sind nicht völlig befriedigend; denn auf eine evidente Art sind sie als Zweckschöpfungen charakterisiert. Von einem natürlichen Logikkalkül im Fregeschen Sinne, aber ohne die widersprucherzeugenden Zulassungen, durch die der Frege-Kalkül gesprengt worden ist, sind auch diese Kalküle noch wesentlich verschieden. Ein natürlicher Logikkalkül wird typenfrei sein müssen wie der mengentheoretische Logikkalkül. Man wird jedoch von einem solchen Kalkül zugleich verlangen müssen, daß er die widersprucherzeugenden Protuberanzen nicht wie dieser durch axiomatische Diktate zum Verschwinden bringt, sondern durch Festsetzungen, die ganz unabhängig von dieser Zielsetzung für das inhaltliche Denken überzeugend sind. Ein einleuchtender Ansatz von dieser Art ist das Prinzip, das besagt, daß ein \(k\)-stelliges Attribut im allgemeinen Falle nicht für alle Ding-\(k\)-tupel, die in einer präzisierten Sprache symbolisiert werden können, sinnvoll ist in dem Sinne, daß es auf ein beliebiges Ding-\(k\)-tupel entweder zutrifft oder \textit{nicht} zutrifft. Dieser Ansatz ist zuerst von \textit{H. Behmann} formuliert worden (Jber. Deutsche Math.-Verein. 40 (1931), 38-48; JFM 57.0056.*). Er ist zugleich mit der wichtigen Entdeckung publiziert worden, daß die übliche Konstruktion der Russellschen Antinomie auf der Verwendung von Kurzzeichen beruht, die nicht eliminierbar sind. Es ist einleuchtend, daß solche Kurzzeichen mindestens im allgemeinen Falle unzulässig sind. Eine Kalkülschöpfung auf dieser Basis hat Behmann jedoch nicht vorgelegt. Dagegen hat \textit{A. Church} nach zwei typenfreien Systemen, die im Sinn dieser Richtlinien angelegt, aber gleichfalls durch widersprucherzeugende Konstruktionsmöglichkeiten gesprengt worden sind, ein drittes System dieser Art geschaffen, für welches die Widerspruchsfreiheit hat gezeigt werden können (Proc. nat. Acad. Sci. USA 21 (1935), 275-281; ``Mathematical logic'', autographiert (Princeton 1935/36); ``The calculi of lambda-conversion'' (Princeton 1941); JFM 61.0055.*; 62\(_{\text{II}}\), 1048 und die nachfolgende Besprechung). Ein sehr bemerkenswerter Effekt dieses Systems ist eine Konstruktion, durch die es gelungen ist, den Ausdruck ``allgemeines Entscheidungsverfahren'' in einem inhaltlich einleuchtenden Sinne so zu präzisieren, daß A. Church auf Grund dieser Präzisierung die Unmöglichkeit eines solchen Verfahrens schon für den beschränkten Prädikatenkalkül der ersten Stufe hat beweisen können. Aber die Ausdrucks- und die Beweismöglichkeiten dieses Systems sind wesentlich beschränkter als die der mengentheoretischen Logikkalküle, und die auf dem Funktionsbegriff fußende Konstruktion dieses Kalküls entfernt sich so weit von den Ansätzen, die man für einen natürlichen Logikkalkül erwartet, daß auch dieses System den unerwünschten Zweckschöpfungen noch zu nahe steht. Die vorliegende Arbeit ist der erste Entwurf eines typenfreien natürlichen Logikkalküls mit sehr weitreichenden Ausdrucks- und Beweismöglichkeiten. Sie will den Leser vor allem vertraut machen mit den Gedanken, die diesem Kalkül zugrunde liegen, und mit der Art, in der diese Gedanken eingegangen sind in die Konstituierung dieses Kalküls. In einem zweiten Teil soll die Widerspruchsfreiheit dieses Kalküls, in einem dritten soll die Leistungsfähigkeit desselben gezeigt werden. Die Arbeit besteht aus vier Paragraphen: \S\ 1. Bemerkungen zur Behmannschen Arbeit, \S\ 2. Grundgedanken des Aufbaus, \S\ 3. Das Axiomensystem, \S\ 4. Herleitungen. Das Hauptproblem von \S\ 2 ist die Frage, welche Zeichenreihen als (sinnvolle) Ausdrücke gelten sollen. Es ergibt sich, daß die sinnvollen Ausdrücke nicht unabhängig von den beweisbaren Formeln oder kürzer: von den Sätzen bestimmt werden können, daß also die Ausdrucks- und Satzbestimmungen, die in den üblichen Konstruktionen getrennt marschieren, so miteinander zu verbinden sind, daß die Ausdrucksbestimmungen teilnehmen an dem im allgemeinen Falle indefiniten Charakter der Satzbestimmungen. Das einfachste Beispiel sind die Ausdrücke, die sich mit Hilfe der aussagenlogischen Verknüpfungen aus gewissen Primformeln erzeugen lassen. In diesem Falle beginnen die Ausdrucksbestimmungen mit der Festsetzung, daß jede beweisbare Formel ein Ausdruck ist. Dann erst folgen die üblichen Bestimmungen. Die leitenden Gedanken sind in vier Leitsätzen formuliert: I (Präzisierung durch A 1, p. 18): Eine Zeichenreihe ohne freie Variablen ist ein \textit{Ausdruck} dann und, nur dann, wenn sie eine Aussage ist in dem Sinn, daß sie entweder wahr oder falsch ist. II (Präzisierung durch A 2, p. 18): Eine Zeichenreihe mit freien Variablen ist ein \textit{Prädikat} dann und nur dann, wenn sie durch wenigstens eine Einsetzung zu einer Aussage ergänzt werden kann. III (Präzisierung CI 15, p. 19): Zu jedem Ding (ich würde den Ausdruck ``Subjekt'' vorziehen) gibt es ein Prädikat, das mit ihm zusammen eine Aussage erzeugt. IV (Präzisierung CII 2. 3, p. 19): Kurzzeichen dürfen im allgemeinen Falle nur dann eingeführt werden, wenn sie eliminierbar sind. Ein paar Druckfehler, auf die ich gestoßen bin, sind unerwünscht, aber nicht fatal.