Logical Tomography - Exposing the Structural Constituents of Logic

Abstract

This thesis is divided into three parts.

The first part is concerned with the origins of structural reasoning. In particular, Paul Hertz' significant influence on Gerhard Gentzen is expounded. It is demonstrated that the structural aspects of Gentzen's sequent calculus are based on a conception of a purely structural reasoning, which had been advocated by Hertz in the 1920s. Some of the particular tenets of Hertz are presented, which amount to a rejection of formal logic. In view of Hertz' strong opinion, the fundamental idea of the sequent calculus, namely to mix structural and formal elements, is critically reviewed.

In the second part, motivated by these historical considerations, a modified sequent calculus is presented. this calculus employs only local variants of the logical rules, i.e. rules in which only a single propositional atom is allowed as contextual formula, and the cut rule that is restricted to propositional variables as cut formulae. The purpose of this calculus, employed in a bottom-up manner, is to successively detach all the complex formula occurrences in a given sequent from their contexts by means of the cut rule and decompose them with the local logical rules. As the initial sequents of derivations obtained by this calculus contain only logical atoms, i.e. no complex formulae, they are called "elementary structural sequents". It is shown that these elementary structural sequents alone contain all the information that is usually expressed by the formulae of the sequent. Moreover, the different paths that can be traced by following matching propositional variables in these sequents, different derivations in the standard sequent calculus can be obtained. Finally, even though the modified calculus is designed to extract elementary sequents instead of constructing proofs, it is possible to decide, whether the original sequent, from which these structural sequents were derived, is provable in the standard sequent calculus or not. It is argued that the set of elementary structural sequents can be considered to express the meaning of the original (formal) sequent.

In the third part, inspired by the methods employed to investigate sets of elementary structural sequent in the second part, a set-theoretical interpretation thereof is suggested: directed cut hypergraphs. After the neccessary notions are introduced (governing e.g. the taxonomy of hyperarcs and traversals in hypergraphs), the interpretation is established and its properties are investigated. Many of these properties can simply be adapted from the results of the second part. The question of deciding the provability of a sequent based on the hypergraph interpretation is addressed in some detail, and a graph-theoretical answer is provided. Finally, a method for directly constructing hypergraphs from Gentzen-style sequents is provided and shown to be equivalent to first obtaining the elementary structural sequents and then relating them to hypergraphs.

Diese Arbeit besteht aus drei Teilen.

Der erste Teil befaßt sich mit den Ursprüngen des strukturellen Räsonnierens. Insbesondere geht es dabei um die Darstellung des erheblichen Einflusses, den Paul Hertz auf Gerhard Gentzen hatte. Es wird gezeigt, daß die strukturellen Aspekte des Gentzenschen Sequenzenkalküls auf der Konzeption einer rein strukturellen Logik basieren, die Hertz in den 20er Jahren des 20. Jahrhunderts vorstellte. Es wird aufgezeigt, daß einige der sonderbar anmutenden Grundannahmen von Hertz als Zurückweisung der formalen Logik verstanden werden können. Vor dem Hintergrund der ausgeprägten Abneigung, die Hertz dagegen verspürte, wird die wesentliche Idee des Sequenzenkalküls, nämlich die, Elemente der strukturellen und der formale Logik zu verbinden, kritisch hinterfragt.

Im zweiten Teil wird, inspiriert von den vorangegangenen historischen Betrachtungen, ein modifizierter Sequenzenkalkül vorgestellt. Dieser Kalkül verwendet nur lokale Varianten der logischen Regeln, d.h. Regeln, in denen als Kontextformel nur eine einzige Aussagenvariable erlaubt ist, sowie die Schnittregel, die als Schnittformeln allerdings nur Aussagenvariable haben darf. Der Zweck dieses Kalküls, dessen Regeln von unten nach oben angewendet werden, besteht darin, nach und nach alle Vorkommen komplexer Formeln in einer gegebenen Sequenz mithilfe der Schnittregel aus ihren Kontexten herauszulösen und mittels der lokalen logischen Regeln zu zerlegen. Da die obersten Sequenzen der Herleitungen in diesem Kalkül nur Atome enthalten, d.h. keine komplexen Formeln, werden sie "elementar-strukturelle Sequenzen" genannt. Es wird gezeigt, daß diese elementar-strukturelle Sequenzen alleine bereits all die Informationen enthalten, die üblicherweise durch Formeln ausgedrückt werden. Darüberhinaus entsprechen die Pfade, die man durch das Verfolgen gleicher Aussagenvariablen in diesen Sequenzen erhält, verschiedenen Herleitungen im gewöhnlichen Sequenzenkalkül. Zuguterletzt kann anhand der elementar-strukturellen Sequenzen entschieden werden, ob die zugrundeliegende Sequenz beweisbar ist oder nicht, obwohl der Kalkül, mit dessen Hilfe diese Sequenzen generiert werden, selbst keine Beweiskraft besitzt. Ausgehend von diesen Eigenschaften wird die Behauptung aufgestellt, daß die Menge der elementar-strukturellen Sequenzen den Sinn der ursprünglichen (formalen) Sequenz zum Ausdruck bringt.

Im dritten Teil wird, basierend auf den Methoden, mittels derer im zweiten Teil Mengen elementar-struktureller Sequenzen untersucht werden, eine mengentheoretische Interpretation dieser Mengen durch gerichtete Hypergraphen vorgeschlagen. Nachdem zunächst die notwendigen Begriffe eingeführt worden sind (die z.B. die Klassifizierung von Hyperkanten und Durchläufen), wird die Interpretation eingeführt und deren Eigenschaften untersucht. Viele dieser Eigenschaften können von den Resultaten des zweiten Teils übernommen werden. Auf die Frage der Entscheidbarkeit der Beweisbarkeit einer Sequenz, basierend auf deren Hypergraphinterpretation, wird ausführlich eingegangen, und eine graphentheoretische Lösung wird dargestellt. Zuletzt wird eine Methode angegeben, die es ermöglicht, aus einer Sequenz direkt einen Hzpergraphen zu konstruieren, und es wird gezeigt, daß dies äquivalent dazu is, erst deren elementar-strukturellen Sequenzen zu generieren und diese durch einen Hypergraphen auszudrücken.