Paul Hertz und seine Grundlegung der strukturellen Beweistheorie

• Antragsteller: Dr. Michael Arndt
• Fachliche Zuordnung: Theoretische Philosophie ; Mathematik ; Theoretische Informatik
• Förderung: Förderung von 2015 bis 2020
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 286620887

In der Vergangenheit gab es zahlreiche Untersuchungen der strukturellen Aspekte des Sequenzenkalküls, so etwa unter dem Oberbegriff der Substrukturellen Logiken und in der Linearen Logik. In jüngster Zeit wurden verschiedene Ansätze zur Rückführung der logischen Aspekte des Sequenzenkalküls auf dessen strukturelles Gerüst vorgeschlagen, etwa in Schroeder-Heisters Kalkül mit Definitorischer Reflektion, in Sambins Basic Logic sowie zuletzt in dem von Tesconi und dem Antragsteller vorgestellten Framework of Explicit Composition. Auch Jean-Yves Girard verfolgt mit seinen Ludics eine ähnliche Zielsetzung; in seiner damit in Verbindung stehenden Theorie einer Geometry of Interaction geht er noch einen Schritt weiter, nämlich sowohl die strukturellen als auch die logischen Aspekte von Sequenzenkalkülen als diskrete Geometrien (Graphen) aufzufassen. Aktuell plädieren Girard und Michele Absrusci für eine "Transzendente Syntax", eine logische Ausdrucksweise, die nicht wie die logische Formelsprache vorab definiert wird, sondern die sich gewissermaßen von selbst aus den elementaren Prinzipien des (logischen) Schließens herauslesen lässt.Die historische Grundlage von Gentzens Sequenzenkalkül ist der Satzkalkül von Paul Hertz. Beschäftigt man sich näher mit Hertz' logischen Arbeiten, so findet man dort zahlreiche der Überlegungen und Meinungen, die den genannten jüngsten Forschungen zugrunde liegen, bereits angelegt. So motivierte Hertz seinen Satzkalkül etwa unter Verwendung geometrischer Anschauungen (und antizipierte dabei nicht nur die Terminologie der Graphentheorie, sondern lieferte auch einige ihrer elementaren Methoden und Ergebnisse). Weiterhin lehnte Hertz die Verwendung logischer Sprache kategorisch mit der Begründung ab, dass sich eine Logik, die sich einer Formelsprache bedient, in Scheinprobleme verstrickt. Hertz war der ausdrücklichen Meinung, dass die Sache der Logik das Räsonieren sei und nicht das Hantieren mit Konventionen.Da die logischen Schriften von Paul Hertz weitgehend unbekannt sind, bleibt sein prägender Einfluss auf aktuelle Fragestellungen im Verborgenen. Das Leitmotiv dieses Projektes ist die Herausarbeitung der Relevanz von Hertz' Arbeiten. Ein wesentlicher Teil des Projektes soll daher darin bestehen, Hertz' Satzkalkül zunächst detailiert darzustellen und sodann dessen Konzepte in ihrer historischen Tragweite, sowohl hinsichtlich der Entwicklung des Gentzenschen Sequenzenkalküls auf der Grundlage des Satzkalküls als auch als Gegenentwurf zur Logik als formales Sprache im Sinne von Russell und Hilbert. In dem anderen Teil des Projektes soll die Relevanz der Annahmen, die Hertz seinem Kalkül zu Grunde legte, für die oben genannten aktuellen Forschungsrichtungen in der strukturellen Beweistheorie dargestellt werden sowie untersucht werden, ob diese Annahmen mit dem Konzept einer transzententalen Syntax vereinbar sind.

• DFG-Verfahren: Sachbeihilfen