Graphs and Hypergraphs in Proof Theory

这个提议的首要主题是使用图进行形式推理，特别是在证明理论中的使用。在19世纪后期出现了几个这样的系统，其中最著名的可能是：（1）维恩图，（2）皮尔士的存在图，（3）弗雷格的概念图。在20世纪用于逻辑的图的例子中有：（4）加德纳的网络图，（5）吉拉德的证明网。最近对这个领域的两个贡献是：（6）休斯的组合证明，（7）格弗斯和勒布的演绎图。不同类型的逻辑图之间的关系，在哲学和逻辑话语中从未被系统地研究过。这是拟议的项目的第一个目标，以实现这一点，通过阐述系统的图论术语（如有向或无向图或超图，双图等）。并利用这个共同的参考框架来阐述这些关系的批判性讨论。特别转向弗雷格、罗素、希尔伯特、赫兹和根岑意义上的传统证明理论，一个值得问的问题是，逻辑形式主义的哪些方面可以用图来有益地呈现。因此，本建议的第二个目的是系统地审查各种传统逻辑系统的结构方面，提供适当的图论渲染，并讨论这种渲染的属性。第一个目标和第二个目标之间几乎没有重叠，因为前者侧重于逻辑图的图形渲染，而后者则针对逻辑系统的那些方面，在很大程度上，从来没有被渲染为图。就逻辑而言，有向超图比有向图更通用。虽然后者足以表示对象之间的关系，但这些关系必须是一对一的类型，而这不足以呈现逻辑中最基本的关系，即逻辑结果，它是多对一的类型。因此，拟议项目的第三个目标是通过将逻辑系统呈现为有向超图来表示逻辑系统的结构特征。这一目标特别适用于已经使用图的微积分、证明网和自然演绎的最新发展。与第一个和第二个目标几乎没有重叠，因为这个目标特别关注使用（有向）超图来改进逻辑演算的图论表示。这一建议的一个特别强调的是使用严格的图论概念（而不是模糊的，仅仅是图形的图表），同时保留一个角度，这是相关的，因为它避免衰减到技术细节。

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.