What could you mean by the term "proof-theoretic semantics" (PTS)? At first glance, it could mean either the semantics of proof theory, or perhaps it's more likely to mean semantics conducted using the tools of proof theory. And that's the enterprise that the fifteen authors intend to advance in the sixteen papers in this edited collection.
The last 70 years has seen the development of a large body of work in formal semantics -- of the tools and techniques of logic finding their way to illuminate and inform semantics of natural language. In this process, not all tools of logic have played an equal part in the application of logic to language. Logic, as the discipline has grown over the 20th and into the 21st Century, has two halves -- model theory and proof theory. You can study logical concepts with a focus on models and representations (think of Tarski's semantics for first order logic, or Kripke models for modal logic), or with a focus on proofs and derivations (think of Hilbert proofs, Fitch-style natural deduction, or Gentzen's sequent calculus). One great logical insight of the 20th Century was to understand this difference clearly, and to show that a vast range of logical consequence relations could be characterised equally in terms of proofs or in terms of models.
If you were to survey the field of formal semantics and dispassionately and objectively account for the ways in which logic has played a role in semantics, one thing would be clear. The overwhelming majority of that work is from the model theory wing of the discipline. This is not because proof theory has nothing to offer. On the contrary: proof theory has seen great strides in the decades since the flowering of the discipline in the work of Hilbert and Gentzen in the early 20th Century. Proof theory has been central in (1) the logical analysis of fundamental mathematical theories like Peano arithmetic and analysis; (2) the development of profound and deep connections between the structure of proofs and the analysis of functions and computation in the lambda calculus, with applications into the semantics of programming languages, and the representation of ever stronger mathematical theories in the recent development of homotopy type theory, and the quest to formalise and encode more and more mathematical reasoning; and (3) the introduction of linear logic, the Lambek calculus of syntactic types, relevant logics, and novel proof theoretic ideas such as proof nets, splitting of logical constants into the additive/extensional, the multiplicative/intensional connectives and the exponentials. This is not only interesting work in logic and its applications to allied disciplines, it is work in which semantics in the rich sense -- issues of meaning and use -- is paramount. So, there is a great deal of scope for the fruitful connection between proof theory and meaning theory.
That rich body of work in proof theory and its myriad applications is not uniformly represented in this volume. This book is not a comprehensive overview of the state of the art in proof theory or even its applications to semantics (that would be impossible in a single volume of a manageable size). It's a more selective work on the state of the art in PTS more narrowly understood: the research program launched in the mid-1980s by one of the editors, Peter Schroeder-Heister, with an aim towards (1) explaining meaning in terms of proof rather than denotation or truth; and (2) giving a semantics for proofs -- giving some kind of account of what it is to be a proof that transcends any particular mode of presentation. This is a relatively more delimited pair of theoretical aims, and it is not surprising that work in this tradition has not stabilised into a period of `normal science' in which there is a small set of established methods and in which teams of researchers work on settled well-defined problems. The authors of papers in this volume (almost all) agree that proof theory is important to semantics, and they mostly agree that this has something to do with natural deduction and the sequent calculus, but beyond that, there is little agreement on the important problems to tackle or on which framework might best be used to tackle those problems. PTS in this narrower sense is very much a field in flux, and this volume shows it.
The volume collects sixteen papers on PTS including an introduction by the editors Thomas Piecha and Schroeder-Heister, and a conclusion setting forth open problems (by Schroeder-Heister), and a critical note "A Strongly Differing Opinion on Proof-Theoretic Semantics?" by Wilfrid Hodges and a reply to Hodges's essay, by Kosta Došen. The remaining twelve papers broach a number of different issues in PTS.
I don't have the space to engage with all of the papers here, but I can summarise them, to give a sense of the range of issues covered. Dag Prawitz's "On the Relation Between Heyting's and Gentzen's Approaches to Meaning" and Walter Dean and Hidenori Kurokawa's "Kreisel's Theory of Constructions, the Kreisel-Goodman Paradox, and the Second Clause" contrast PTS with other traditions in constructive semantics (Heyting's interpretation of intuitionistic logic, for Prawitz, and Kreisel and Goodman's, for Dean and Kurokawa); Roy Dyckhoff's "Some Remarks on Proof-Theoretic Semantics" is a critical examination of approaches in proof-theoretic semantics based on the program of "General Elimination Harmony". Gabriele Usberti's "The Paradox of Knowability from an Intuitionistic Standpoint" proposes a solution to the epistemic knowability paradox from the standpoint of logic. This is an exotic proposal to "solve" the knowability paradox by admitting that if p, then Kp, on intuitionist lines. Frankly, there is not a great deal of PTS in this paper. In "Towards a Proof-Theoretic Semantics of Equalities," Reinhard Kahle applies proof-theoretic semantics to the treatment of equality by elucidating the difference between extensional and intensional equality in a non-denotational way. Lars Hallnäs sketches some ideas towards a proof-theoretic foundation for set theory using generalisations of definitional reflection.
Warren Goldfarb's "On Dummett's 'Proof Theoretic Justification of Logical Laws'" has been circulating for more than fifteen years and has been referred to repeatedly in the philosophical literature on proof theory. It was the subject of Dummett's presentation at the first PTS conference in 1999. It is good to have this paper in print, at last. Jan Ekman's "Self-contradictory Reasoning" is an attempt to analyse non-well founded and paradoxical reasoning from a proof theoretic perspective. Piecha's "Completeness in Proof-Theoretic Semantics" gives an account of different completeness notions salient in proof theoretic semantics (chiefly due to Prawitz), which aim to show that the logical rules in a system completely characterise validity in that system, where validity itself is given a proof-theoretic analysis. This is more informative and less circular than it seems, because the general notion of validity of an argument is not to be identified with the presence of a proof from the premises to the conclusion, but a more rigorous notion, for which completeness becomes a significant and contested question. The volume ends with a presentation from Schroeder-Heister of three significant open questions for the development of Proof-Theoretic Semantics.
I will discuss the papers that remain in some greater depth, together with Došen's response to Hodges.
First, let's consider the two papers in which the mathematical formalism of category theory plays a crucial role. First, Došen, in "On the Paths of Categories" pleads for an approach to proof-theoretic semantics in which category theory is central, arguing that category theory best exhibits the structures of deductions. This is an important theme in the literature on PTS, because of the ever present need to give an account of the core notions of proof theory in a way which abstracts away from the syntactic representation. We have a notion of model for a formal language which goes some way to abstract away from the particular tools of representation of the model. (Two presentations of models are presentations of the same model if and only if they have the same domain and the interpretations of the non-logical vocabulary agree, whether you think of the interpretation of a predicate as a set of instances, a relation, a function or whatever. We have no such straightforward and agreed-upon answer as to when two different syntactic representations of a proof -- say in natural deduction, or a tableaux or a Hilbert proof -- represent the same connection between the premises and the conclusion.) The mathematical domain of categories -- the abstract theory of objects and 'arrows' between them satisfying some basic core conditions -- is a good fit for at least a general, syntax-independent account of proofs from one premise to one conclusion, and Došen (with his colleague Zoran Petrić) has explored this connection in some great detail over the last twenty years. One theme of the paper is that the transition from single premise-single conclusion proof objects to multi-premise single-conclusion proofs (in multicategories) and multiple-premise multiple-conclusion proofs (in polycategories) are also possible, but come with their own costs as well as their benefits. Došen states in an aside that these "plural deductions of classical logic are not very natural. They have been invented following Gentzen's suggestion, and not found by describing deduction in real life" (p. 74). This sort of remark is often made in discussions of proof structures and their applications, without much attention to how one might find 'deduction in real life' and how proof structures are to be related to reasoning in natural language (or wherever deductive reasoning is to be found). More work needs to be done on the interface between natural language and abstract proof structures, and the kinds of deductive connections to be found in "deduction in real life."
In his paper, Došen argues not only that categories are a fruitful home for understanding the core logical content of the notion of a proof, but also that we should admit into our view the notion that the objects of proof need not only be propositions, but also other speech act types, such as commands and questions. This is an important point, and one that is worth emphasising. The kinds of transitions found in proofs (such as making and then discharging hypotheses, and moving from instances to generalisations) seem to involve more than flat assertions which express the belief commitments of the one proposing the proof. There is not only scope for exploring the semantics of different kinds of speech acts in terms of proof theory, but this is a necessity for anyone that proposes a proof-theoretic semantics in anything like a comprehensive sense for natural language. While both the model-theoretic and proof-theoretic traditions have kept assertions as the central topic of analysis, natural language meaning involves much more than the semantics of assertions. Došen's paper reminds us that we should not only hope for more, but that proof theory gives us the tools for more.
The connection with category theory is sustained also in Yoshihiro Maruyama's suggestive paper "Categorical Harmony and Paradoxes in Proof-Theoretic Semantics", which gives a taxonomy of various forms of paradoxes based on a categorial approach to proof-theoretic harmony. This paper is an exploration of different forms of paradoxicality, including seemingly paradoxical concepts which appear to be defined by defective inference rules (like Prior's infamous "tonk"), and the more widely known paradoxes like the Liar and Russell's paradox. Maruyama proposes a notion of "harmony" (a criterion for a family of rules to appropriately define logical concepts) and he shows that certain well behaved concepts are harmonious while other badly behaved concepts are not (as one would hope), but that there are grades of paradoxicality -- different defective concepts (like tonk, and a statement definitionally equivalent to its own negation, akin to Russell's paradox) are situated at different points along the scale. This is some elegant formal characterisation, but questions remain about how the formal results are to be applied in semantics more generally. As I have mentioned, Maruyama's results are couched in the language of category theory -- to be more specific, in the monoidal categories studied in the semantics of linear and other substructural logics. (The details of monoidal category theory are not important to understand the point.) A monoidal category is not only equipped with a family of proofs from single premise to single conclusion (as in Došen's paper), which may be chained together (a proof p from A to B, chained with a proof q from B to C gives us a proof (p o q) from A to C). In monoidal categories we have a kind of parallel composition, in which a proof r from A to B can be parallel composed with a proof s from C to D into a proof (r ⊗ s) from (A ⊗ C) to (B ⊗ D). (These two forms of composition have to satisfy different kinds of sanity conditions which we need not discuss here.) Monoidal categories are an interesting formal structure, and they have some elegant and important mathematical features. However, when it comes to their application to natural language semantics, more work must be done if we are to understand their significance. In particular, Maruyama helps himself to the notion of a monoidal category without ever asking what the parallel composition operator is meant to mean. Look at the conditions we have specified: For all that's been said, (A ⊗ C) could be the disjunction of A and C, their conjunction, or many other things besides. More must be done if we are to apply the formal tools of monoidal category theory and understand how they deliver results.
Jan von Plato's "Explicit Composition and Its Application in Proofs of Normalization" is a gem of a paper. It has arisen out of von Plato's detailed work on Gentzen's development of natural deduction and the sequent calculus. This paper investigates a new formulation of natural deduction and sequent calculus in which there is an explicit proof step of composition, in order to highlight a difference between ways that fundamental properties of proofs can be demonstrated. Proofs are inductively defined objects. You define the basic proofs and then show how, given a proof, you can extend it by way of a new step, into a new, larger proof. Properties of proofs are often proved inductively in the same way, but some crucial properties (in particular, normalisation, or cut-elimination), are proved inductively, but not by way of an induction on the structure of the proof -- but a much more complex induction. Von Plato's system with an explicit composition rule allows for a presentation of proof structure which allows for key properties (including normalisation and strong normalisation) to be proved by an induction on the structure of proof. This elegant paper is a demonstration of the options available even at the core level of the discipline. Gentzen's own rules for the sequent calculus were the result of design choices, and von Plato shows that different design choices give us proof systems with different fundamental properties.
The most curious papers in the volume are the exchange between the respected model theorist Wilfrid Hodges and the proof theorist Kosta Došen, in Hodges' "A Strongly Differing Opinion on Proof-Theoretic Semantics?" and Došen "Comments on an Opinion". This short pair of papers is an important presence, despite (or perhaps because of) the prickly tone in the back and forth between Hodges and Došen. Hodges "differing opinion" starts by explaining that the rhetoric from the proponents of PTS on the difference between model theory and proof theory paints a picture of model theory that Hodges, as a model theorist, does not recognise. Chief, in Hodges response, is his recognition that model theoretic accounts of logical consequence and model theoretic accounts of meaning are different, though related, enterprises. Tarski and his intellectual descendants developed tools for the analysis of logical consequence by way of models. It is another thing entirely to offer model theoretic analysis of meaning. Hodges gives some good examples of the difficulties and subtleties involved in giving a formal account (model theoretically or by some other means) of the meaning of natural language expressions, like "and", whose significance varies from context to context. Došen, in reply, concedes some of the points made by Hodges, and resists on others. Došen's conclusion defends his view of the primacy of deductions over propositions (of inference over assertion), and at this point, it is clear that there is not a disagreement between Došen and Hodges, but a fundamental distinction of vocabularies. Hodges ends his differing opinion "In the mainstream semantic and model-theoretic literature that I've seen, nobody talks about 'prior' notions or about one notion having 'primacy' over another." As Došen clearly explains, for Dummett (and I'd add, for Brandom, and others in the normative pragmatic tradition) questions of priority of concepts are central. For Dummett, "Frege's account, if it is to be reduced to a slogan, could be expressed in this way: that in the order of explanation the sense of a sentence is primary, but in the order of recognition the sense of a word is primary" (Dummett, M. A. E., Frege: Philosophy of Language, Duckworth 1973, Chapter 1). The back and forth between Hodges and Došen is difficult, and at times testy. However, it is a clear demonstration of the kinds of miscommunication and differences of approach between different traditions in the application of logic to theories of meaning. There is precious little shared ground at the end of the exchange, but this pair of papers at least helps to get some of the difficulties out in the open.
As for this pair of papers, so for the volume as a whole. There are many ideas and approaches on display, with some shared themes and techniques, but there is not so much in the way of coherent and developed methodology. I can only hope there is more to come in this tradition, because there are connections to be made between meaning, use, rules and inference. This collection is an important part of what will prove to be a long journey. We can hope that it sparks more interest in the possibilities for proof theory in its application to theories of meaning, and that in future work, we have more self reflection on the fundamentals of how the notions of proof are connected to language use and understanding, and what tools make those connections most clear, and more work on the range of applications in the theory of meaning for speech acts beyond assertion and concepts beyond the core logical constants. Then we will truly have made advances PTS, and this volume would have played its part.