Advances in Proof-Theoretic Semantics: Introduction

Abstract As documented by the papers in this volume, which mostly result from the second conference on proof-theoretic semantics in Tübingen 2013, proof-theoretic semantics has advanced to a well-established subject in philosophical logic.

Keywords Proof-theoretic semantics

In the mid-1980s, the term “proof-theoretic semantics” (Schroeder-Heister 1991 [13], and before in lectures) was proposed (1) to explain meaning in terms of proof rather than denotation or truth and (2) to give a semantics for proofs. Though related to the meaning-as-use approach in the philosophy of language, and belonging to what in a more general setting has been called “inferentialism” (Brandom 1994 [1]), the intention of proof-theoretic semantics was to capture and continue the specific line of research that originated from the work of Gentzen (1934/35) [5] (and also Jas´kowski 1934 [6]) and was taken up and developed, amongst others, by Lorenzen (1955) [8], Prawitz (1965, 1971) [11, 12], von Kutschera (1968) [15], Martin-Löf

(1975, 1984) [9, 10], and Dummett (1975, 1991) [2, 3]. Whereas in the 1980s prooftheoretic semantics was almost exclusively the business of proof-theorists, the field has since expanded into the wider area of philosophical logic. The first conference on proof-theoretic semantics was held in 1999 in Tübingen with a special issue of Synthese originating from it, which was published in 2006 (Kahle and SchroederHeister 2006 [7]). At the time of this first conference, the subject still belonged to a relatively small community of logicians and philosophers. This has changed in the meantime. One only needs to look at the multitude of papers published on issues of proof-theoretic semantics in the past decade and at the widespread usage of this term. “Proof-theoretic semantics” is no longer the provocative title it used to be, containing an alleged contradictio in adjecto between proof theory as dealing with syntax, and semantics as dealing with meaning. The link between proofs and meaning is well-established now. Given the growing interest in the subject, we organised a second conference on proof-theoretic semantics in Tübingen in 2013 to discuss the advances in the now well-established field (for overviews see Wansing 2000 [16], Schroeder-Heister 2012 [14]). Some speakers of the second conference had already spoken at the first, namely Došen, Dyckhoff, Hallnäs, Kahle, Prawitz, Sundholm, Tait and Usberti.

The presentations given at the conference were the following.

• Sergei N. Artëmov: On Brouwer-Heyting-Kolmogorov provability semantics

• Walter Dean and Hidenori Kurokawa: Kreisel's second clause and the Theory of


• Kosta Došen: Two ways of general proof theory

• Roy Dyckhoff: Generalised elimination rules

• Lars Hallnäs: On the proof-theoretic foundations of set theory

• Wilfrid Hodges: The choice of semantics as a methodological question

• Reinhard Kahle: The mode of presentation

• Yoshihiro Maruyama: On paradoxes in proof-theoretic semantics

• Jan von Plato: Explicit composition and its application in normalization proofs

• Dag Prawitz: Remarks on relations between Gentzen and Heyting inspired PTS

• Giovanni Sambin: Unification of logics by reflection

• Göran Sundholm: BHK and Brouwer's theory of the creative subject

• William W. Tait: Compositional semantics for predicate logic: Eliminating bound

variables from formulas and deductions

• Gabriele Usberti: Intuitionism, the Paradox of Knowability and empirical negation

• Heinrich Wansing: A two-sorted typed lambda-calculus

This volume collects the contributions of many of the participants, not necessarily in the form presented, and also some additional papers by authors who did not speak at the conference. Therefore it exemplifies from many perspectives what proof-theoretic semantics is about. The papers by Prawitz and Dean and Kurakowa confront the proof-theoretic approach with the constructive semantics of Heyting and of Kreisel and Goodman, respectively. Došen pleads for a categorial approach to proof-theoretic semantics, arguing that it best exhibits the structures of deductions. Dyckhoff's paper is a critical examination of approaches in proof-theoretic semantics based on general elimination rules of a certain form. Maruyama gives a taxonomy of various forms of paradoxes based on a categorial approach to proof-theoretic harmony. Usberti proposes a solution to the epistemic knowability paradox from the standpoint of logic. Von Plato investigates the significance of a rule of explicit composition in natural deduction which makes the substitution of a derivation for an open assumption an inference step of its own. Kahle applies proof-theoretic semantics to the treatment of equality by elucidating the difference between extensional and intensional equality in a non-denotational way. Hallnäs sketches some ideas towards a proof-theoretic foundation for set theory using generalisations of definitional reflection. The paper by Hodges, which is the only one not written from the perspective of a proof-theoretic semanticist or constructivist, defends model theory against false claims from the proof-theoretic semantics 'camp'. It is followed by a reply by Došen.

Goldfarb's paper has been circulating for more than 15 years and has been referred to repeatedly. It was the subject of Dummett's presentation at the first conference in 1999. It represents significant results on the proof-theoretic semantics of intuitionistic logic, in particular on the question of completeness. Another contribution not presented at the conference is a chapter of Ekman's thesis (Ekman 1994 [4]). It uses an interesting way of associating labels with formulas that are proved, which is different from standard Curry–Howard term-annotation and particularly suited to analyse non-well-founded and paradoxical reasoning, a topic which has recently gained much attention in the proof-theoretic semantics community. There are also papers by us, the editors: An overview on results concerning completeness in prooftheoretic semantics and a presentation of three open problems that are considered significant for the further development of the subject.

We would like to thank all participants of the conference, and in particular all contributors to this volume, who made this work possible, as well as those who helped with reviewing and editing the papers. We are also very grateful to Marine Gaudefroy-Bergmann for invaluable organisational assistance. The second editor is particularly grateful to Reinhard Kahle and Thomas Piecha, who organised the conference as a present for his 60th birthday including a special colloquium with friends and colleagues.

Acknowledgments This work was supported by the French-German ANR-DFG project “Hypothetical Reasoning—Its Proof-Theoretic Analysis” (HYPOTHESES), DFG grant Schr 275/16-2. Its completion was supported by the French-German ANR-DFG project “Beyond Logic: Hypothetical Reasoning in Philosophy of Science, Informatics, and Law”, DFG grant Schr 275/17-1.

< Prev   CONTENTS   Next >