Paul Hertz and his Foundation of Structural Proof Theory

点击翻译按钮获取中文摘要

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.