In Prawitz’s semantics, the validity of an argument may be defined, either relatively to an atomic base which determines the meaning of the non-logical terminology, or relatively to the whole class of atomic bases, namely as logical validity. In the first case, which may be qualified as local, one has to choose whether validity of arguments is or not monotonic over expansions of bases, while in the second case, which may be qualified as global, one has to choose whether the (...) reduction functions which justify non-primitive inferences are or not base-depending. I claim that these oppositions enjoy some conceptual symmetries, and that these symmetries may be understood as putting restrictions on one’s choice both at the local and at the global level. This produces two different proof-theoretic semantics in line with Prawitz’s tenets. However, I also argue that the symmetries stem from a deeper interaction within Prawitz’s semantics, i.e. non-logical meanings vs interpretation of rules. This interaction is in turn based on some primitive ingredients which, when suitably combined, produce other two Prawitz-compatible readings. The four readings form a diagram where some order relations hold. I finally claim that this diagram is complete, namely that, if we combine the ingredients in ways other than those giving rise to the four readings above, we obtain nothing new, or nothing compatible with general semantic requirements. Thus, symmetries between the local and the global level, and interaction between non-logical meaning and interpretation of rules, produce a complete classification of potential Prawitzian semantics. (shrink)

We outline a class of term-languages for epistemic grounding inspired by Prawitz’s theory of grounds. We show how denotation functions can be defined over these languages, relating terms to proof-objects built up of constructive functions. We discuss certain properties that the languages may enjoy both individually and with respect to their expansions. Finally, we provide a ground-theoretic version of Prawitz’s completeness conjecture, and adapt to our framework a refutation of this conjecture due to Piecha and Schroeder-Heister.

We define a class of formal systems inspired by Prawitz’s theory of grounds. The latter is a semantics that aims at accounting for epistemic grounding, namely, at explaining why and how deductively valid inferences have the power to epistemically compel to accept the conclusion. Validity is defined in terms of typed objects, called grounds, that reify evidence for given judgments. An inference is valid when a function exists from grounds for the premises to grounds for the conclusion. Grounds are described (...) by formal terms, either directly when the terms are in canonical form, or indirectly when they are in non-canonical form. Non-canonical terms must reduce to canonical form, and two terms may be said to be equal when they converge towards equivalent grounds. In our systems these properties can be proved through rules distinguished according to whether they concern types or logic. Type rules involve type introduction and elimination, equality for application of operational symbols, and re-writing equations for non-canonical terms. The logic amounts to a sort of intuitionistic system in a Gentzen format. To conclude, we show that each system of our class enjoys a normalization property. (shrink)

This open access book is a superb collection of some fifteen chapters inspired by Schroeder-Heister's groundbreaking work, written by leading experts in the field, plus an extensive autobiography and comments on the various contributions by Schroeder-Heister himself. For several decades, Peter Schroeder-Heister has been a central figure in proof-theoretic semantics, a field of study situated at the interface of logic, theoretical computer science, natural-language semantics, and the philosophy of language. -/- The chapters of which this book is composed discuss the (...) subject from a rich variety of angles, including the history of logic, the proper interpretation of logical validity, natural deduction rules, the notions of harmony and of synonymy, the structure of proofs, the logical status of equality, intentional phenomena, and the proof theory of second-order arithmetic. All chapters relate directly to questions that have driven Schroeder-Heister's own research agenda and to which he has made seminal contributions. The extensive autobiographical chapter not only provides a fascinating overview of Schroeder-Heister's career and the evolution of his academic interests but also constitutes a contribution to the recent history of logic in its own right, painting an intriguing picture of the philosophical, logical, and mathematical institutional landscape in Germany and elsewhere since the early 1970s. The papers collected in this book are illuminatingly put into a unified perspective by Schroeder-Heister's comments at the end of the book. Both graduate students and established researchers in the field will find this book an excellent resource for future work in proof-theoretic semantics and related areas. (shrink)

The contributions to this volume represent a broad range of aspects of proof-theoretic semantics. Some do so in the narrower, and some in the wider sense of the term. Some deal with issues I have been concerned with directly, and some tackle further problems. All of them open interesting new perspectives and develop the field in different directions. I will briefly comment on the significance of each contribution here.

It is argued that the intuitionistic conception of negation as implication of absurdity is inadequate for the proof-theoretic semantic analysis of negative predication and distinctness. Instead, it is suggested to construe negative predication proof-theoretically as subatomic derivation failure, and to define distinctness—understood as a qualified notion—by appeal to negative predication. This proposal is elaborated in terms of intuitionistic bipredicational subatomic natural deduction systems. It is shown that derivations in these systems normalize and that normal derivations have the subexpression (incl. subformula) (...) property. A proof-theoretic semantics for negative predication and distinctness is defined, and an intuitionistic conception of truth based on canonical derivations is proposed. An application to the doctrine of the Trinity, to which negative predication and distinctness are central, illustrates the systems and their proof-theoretic semantics. (shrink)

Prawitz conjectured that proof-theoretic validity offers a semantics for intuitionistic logic. This conjecture has recently been proven false by Piecha and Schroeder-Heister. This article resolves one of the questions left open by this recent result by showing the extensional alignment of proof-theoretic validity and general inquisitive logic. General inquisitive logic is a generalisation of inquisitive semantics, a uniform semantics for questions and assertions. The paper further defines a notion of quasi-proof-theoretic validity by restricting proof-theoretic validity to allow double negation elimination (...) for atomic formulas and proves the extensional alignment of quasi-proof-theoretic validity and inquisitive logic. (shrink)

This special issue on general proof theory collects papers resulting from the conference on general proof theory held in November 2015 in Tübingen.