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.