Graphs and Hypergraphs in Proof Theory

• Applicant: Dr. Michael Arndt
• Subject Area: Theoretical Philosophy
• Term: from 2019 to 2023
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 419157690

The overarching theme of this proposal is the use of diagrams for the purpose of formal reasoning and, especially, their use in proof theory. Several systems of this kind were presented in the late 19th century, perhaps most notably among them:(1) Venn’s diagrams,(2) Peirce’s existential graphs,(3) Frege’s Begriffsschrift.Among the examples of diagrams used for logic in the 20th century are:(4) Gardner’s network diagrams,(5) Girard’s proof nets.Two of the very recent contributions to this field are:(6) Hughes’ combinatorial proofs,(7) Geuvers’ and Loeb’s deduction graphs.The relationships between different kinds of logical diagrams, have never been systematically investigated in the philosophical and logical discourse. It is the first aim of the proposed project to accomplish this by explicating the systems in the terminology of graph theory (e.g. as directed or undirected graphs or hypergraphs, bigraphs etc.) and utilizing this shared frame of reference to elaborate a critical discussion of these relationships. Turning specifically to traditional proof theory in the sense of Frege, Russell, Hilbert, Hertz and Gentzen, a worthwhile question to ask is which aspects of logical formalisms could be gainfully rendered by graphs. A second aim of this proposal is thus to systematically review the structural aspects of various traditional logical systems, to provide adequate graph theoretical renderings, and to discuss the properties of such renderings. There is little overlap between the first aim and this one, since the former focuses on graph renderings of logical diagrams, whereas the latter aims at those aspects of logical systems that have, for the largest part, never been rendered as diagrams.For the purpose of logic, directed hypergraphs are significantly more versatile than directed graphs. While the latter are sufficient for representations of relationships between objects, those relationships must necessarily be of the type one to one, and this is inadequate for the purpose of rendering the most fundamental relation in logic, namely logical consequence, which is of the type many to one. The third aim of the proposed project is thus to represent structural features of logical systems by rendering them as directed hypergraphs. This aim particularly applies to the sequent calculus, proof nets and recent developments in natural deduction that already make use of graphs. There is little overlap with the first and second aim, as this one specifically focusses on using (directed) hypergraphs to improve graph theoretical representations of logical calculi. A particular emphasis of this proposal is to use rigorous graph theoretical notions (instead of vague and merely graph-like diagrams) while at the same time retaining a perspective that is philosophically relevant in that it avoids decaying into technicalities.

• DFG Programme: Research Grants