Graphen und Hypergraphen in der Beweistheorie

• Antragsteller: Dr. Michael Arndt
• Fachliche Zuordnung: Theoretische Philosophie
• Förderung: Förderung von 2019 bis 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 419157690

Das übergreifende Thema dieses Vorhabens ist die Verwendung von Diagrammen zum Zwecke des formalen Räsonierens, insbesondere deren Anwendung in der Beweistheorie.Im ausgehenden 19. Jahrhundert wurden diverse Systeme dieser Art vorgestellt. Die wichtigsten darunter sind wohl:(1) Venn-Diagramme,(2) Peircesche existenzielle Graphen,(3) Freges Begriffsschrift.Zu den Beispielen aus der Logik des 20. Jahrhunderts zählen:(4) Gardners Netzwerkdiagramme,(5) Girards Beweisnetze.Zwei der jüngeren Beiträge zu diesem Gebiet sind:(6) Hughes' Kombinatorische Beweise,(7) Geuvers' und Loebs Herleitungsgraphen.Die Beziehungen zwischen verschiedenen Arten logischer Diagramme sind im logischen und philosophischen Diskurs bisher nicht systematisch untersucht worden. Ein erstes Ziel dieses Vorhabens besteht daher darin, diese Zusammenhänge systematisch zu untersuchen. Um eine kritische Diskussion in einem gemeinsamen Rahmen überhaupt zu ermöglichen, sollen die untersuchten Systeme in geeigneten Begriffen der Graphentheorie dargestellt werden (z.B. als gerichtete oder ungerichtete Graphen bzw. Hypergraphen, Bigraphen).Des weiteren soll in Bezug auf die traditionelle Beweistheorie im Sinne von Frege, Russell, Hilbert, Hertz and Gentzen die Frage gestellt werden, welche Aspekte logischer Formalismen nutzbringend als Graphen dargestellt werden können. Ein zweites Ziel dieses Vorhabens besteht somit darin, die strukturhaften Elemente verschiedener traditioneller logischer Kalküle dahingehend zu untersuchen, ob eine graphentheoretische Darstellung sinnvoll ist, und im positiven Fall deren Eigenschaften zu diskutieren. Im Gegensatz zum ersten Ziel soll es hierbei nicht darum gehen, Klassen logischer Diagramme als Graphen auszudrücken, sondern vielmehr darum, Aspekte logischer Formalismen, die bisher nicht diagrammatisch ausgedrückt wurden, als Graphen darzustellen. Für die Anforderungen der Logik haben Hypergraphen gegenüber konventionellen Graphen einen weitaus höheren Nutzen. Letztere eignen sich zwar zur Darstellung einfacher Beziehungen zwischen Gegenständen, aber diese Beziehungen sind notwendigerweise vom Typ 1:1. Allerdings reicht dies schon zum Zwecke einer Darstellung der grundlegenden Beziehung in der Logik, der Konsequenzrelation, nicht aus, da diese den Typ n:1 hat. Das dritte Ziel dieses Vorhabens besteht daher darin, strukturelle Eigenschaften logischer Systeme als gerichtete Hypergraphen darzustellen. Dies betrifft insbesondere den Sequenzenkalkül, Beweisnetzte sowie jüngste Entwicklungen für den Kalkül des natürlichen Schließens, welche bereits graphische Repräsentationen nutzen. Da dieses Ziel im Besonderen (gerichtete) Hypergraphen nutzt, um graphische Darstellungen logischer Kalküle zu verbessern, sollte es keine nennenswerte Überschneidung mit dem zweiten Ziel geben. Das Vorhaben hat den Anspruch, jeweils präzise graphentheoretische Begriffe zu verwenden, dabei allerdings eine Perspektive zu wahren, die philosophisch relevant ist.

• DFG-Verfahren: Sachbeihilfen