Paul Hertz and his Foundation of Structural Proof Theory

对序列演算的结构方面有许多研究，其中一些在“子结构逻辑”的标题下收集，另一些在线性逻辑的相关领域。最近，人们提出了几种不同的方法，其共同目标是建立顺序微积分逻辑方面的结构基础，例如Schroeder-Heister的定义反射微积分，Sambin的基本逻辑以及最近由Tesconi和申请人提出的显式组合框架。Jean-Yves Girard在ludics方面也在追求类似的目标，他的交互几何相关理论更进一步，用离散几何（即图）来解释顺序演算的结构和逻辑方面。最近，Girard和Michele Abrusci提出了一种“先验语法”，这是一种逻辑表达模式，它不仅像公式化的逻辑语言那样被定义，而且可以从（逻辑）推理的基本原则中提取出来。历史上，根岑的序贯演算是在保罗·赫兹的句子演算的基础上发展起来的。仔细考虑赫兹的逻辑工作，就会发现它们是基于审议和估计的，这些审议和估计与上述最近研究中必不可少的研究非常相似。举个例子，赫兹的句子演算的灵感来自于几何理解（他不仅预言了图论的术语，还提供了图论的几个基本方法和结果）。此外，赫兹拒绝使用逻辑语言，理由是使用形式语言的逻辑会分心，并陷入由形式语言产生的问题中。赫兹在他的观点中很明确，逻辑的主题应该是推理，而不是忙于惯例。由于保罗·赫兹的逻辑著作在很大程度上仍不为人所知，他对与当前研究直接相关的问题的形成性影响仍然难以理解。这个项目的主题是阐述赫兹工作的相关性。该项目的一个重要部分包括对句子演算的详细介绍和对其基本原则的历史作用的彻底讨论，一方面是关于根岑将句子演算进一步发展为顺序演算，另一方面是他们明确反对罗素和希尔伯特意义上的逻辑作为一种形式语言的概念。该项目的另一部分致力于展示和检验赫兹的概念与前面提到的结构证明理论的当前趋势的相关性，特别关注先验句法的概念。

There have been numerous investigations into the structural aspects of the sequent calculus, some of them collected under the heading "substructural logics", others in the related field of linear logic. More recently, several different approaches with the common aim of establishing a structural foundation of the sequent calculus' logical aspects have been suggested, for instance Schroeder-Heister's calculus with definitional reflection, Sambin's Basic Logic and most recently the framework of explicit composition that was recently proposed by Tesconi and the applicant. Jean-Yves Girard is pursuing a similar goal with ludics, and his related theory of a geometry of interaction goes one step further by interpreting both structural and logical aspects of sequent calculi in terms of discrete geometries (i.e.graphs). Most recently, Girard and Michele Abrusci have proposed a "transcendental syntax", a logical mode of expression that is not merely defined like a formulaic logical language but that can rather be extricated from the elementary principles of (logical) reasoning.Historically, Gentzen's sequent calculus was developed on the basis of Paul Hertz' sentence calculus. A closer consideration of Hertz' logical works reveals that they are based on deliberations and estimations that are quite similar to those which are essential in the above mentioned recent research. For one example, Hertz motivated his sentence calculus by appealing to geometrical apprehension (and anticipated not only the terminology of graph theory but also provided several of its elementary methods and results). Moreover, Hertz repudiated the utilization of logical language on the grounds that a logic that employs a formal language becomes distracted and ensnared in problems that arise from and revolve around that language. Hertz was explicit in his opinion that the subject matter of logic should be reasoning rather than busying oneself with conventions.Since the logical writings of Paul Hertz are still largely unknown, his formative impact on questions directly relating to current research remains inaccessible. The main theme of this project is to elaborate the relevance of Hertz' work. An important part of the project consists in a detailed presentation of the sentence calculus and a thorough discussion of the historical agency of its fundamental tenets, for one regarding the further development of the sentence calculus into the sequent calculus by Gentzen, but also in their explicit opposition to the notion of logic as a formal language in the sense of Russell and Hilbert. The other part of the project is dedicated to presenting and examining the relevance of Hertz' conceptions to the aforementioned current trends in structural proof theory with a particular focus on the notion of transcendental syntax.