A formulation of the simple theory of types. (Q2589521)

Verf. formalisiert die einfache Typentheorie, wobei er einen Teil des \(\lambda\)-Konversionskalküls mitnimmt. Er bemerkt, daß es nicht möglich ist, den ganzen \(\lambda\)-Kalkül mitzunehmen, falls \(\lambda\) die Bedeutung eines Abstraktionsoperators und Nebeneinanderstellung ihre Bedeutung als die Beziehung von Funktion zu Argument behalten sollen. Die Symbole ı\ und \(\circ\) stellen die Grundtypen, Individuum und Aussage, dar. Sind \(\alpha\) und \(\beta\) Typen, so ist \((\alpha\beta)\) der Typus einer Funktion mit Argument vom Typus \(\beta\) und Funktionswert vom Typus \(\alpha\). Funktionen mehrerer Variablen sind im Sinne \textit{Schönfinkel}s (Math. Ann., Berlin, 92 (1924), 305-316; F. d. M. 50, 23) zu verstehen. Die natürlichen Zahlen werden als Abkürzungen für gewisse \(\lambda\)-Ausdrücke eingeführt. Das System hat sechs Schlußregeln. Die drei ersten stellen die Regeln der \(\lambda\)-Konversion dar; die anderen sind die Abtrennungs-, die Einsetzungs- und eine Generalisationsregel. Weiter hat das System 11 formale Axiome, von denen die vier ersten die Axiome des klassischen Aussagenkalküls sind (\textit{Hilbert-Ackermann}, Grundzüge der theoretischen Logik (2. Aufl. 1938; F. d. M. \(64_{\text I}\), 26), S. 23), die sechs ersten für den Prädikatenkalkül genügen, und die neun ersten für die elementare Zahlentheorie hinreichend sind. Drei der Peanoschen Axiome für die Arithmetik folgen bereits aus den sechs ersten Axiomen des Systems. Einige Theoreme für beliebige Typen werden bewiesen und zum Schluß die Formalisierung der Definition durch primitive Rekursion innerhalb des Systems gezeigt.