We begin with a brief explanation of our proof-theoretic criterion of paradoxicality—its motivation, its methods, and its results so far. It is a proof-theoretic account of paradoxicality that can be given in addition to, or alongside, the more familiar semantic account of Kripke. It is a question for further research whether the two accounts agree in general on what is to count as a paradox. It is also a question for further research whether and, if so, how the so-called Ekman (...) problem bears on the investigations here of the intensional paradoxes. Possible exceptions to the proof-theoretic criterion are Prior’s Theorem and Russell’s Paradox of Propositions—the two best-known ‘intensional’ paradoxes. We have not yet addressed them. We do so here. The results are encouraging. §1 studies Prior’s Theorem. In the literature on the paradoxes of intensionality, it does not enjoy rigorous formal proof of a Gentzenian kind—the kind that lends itself to proof-theoretic analysis of recondite features that might escape the attention of logicians using non-Gentzenian systems of logic. We make good that lack, both to render the criterion applicable to the formal proof, and to see whether the criterion gets it right. Prior’s Theorem is a theorem in an unfree, classical, quantified propositional logic. But if one were to insist that the logic employed be free, then Prior’s Theorem would not be a theorem at all. Its proof would have an undischarged assumption—the ‘existential presupposition’ that the proposition $$\forall p(Qp\!\rightarrow \!\lnot p)$$ ∀ p ( Q p → ¬ p ) exists. Call this proposition $$\vartheta $$ ϑ. §2 focuses on $$\vartheta $$ ϑ. We analyse a Priorean reductio of $$\vartheta $$ ϑ along with the possibilitate $$\Diamond \forall q(Qq\!\leftrightarrow \!(\vartheta \!\leftrightarrow \! q))$$ ◊ ∀ q ( Q q ↔ ( ϑ ↔ q ) ). The attempted reductio of this premise-pair, which is constructive, cannot be brought into normal form. The criterion says we have not straightforward inconsistency, but rather genuine paradoxicality. §3 turns to problems engendered by the proposition $$\exists p(Qp\wedge \lnot p)$$ ∃ p ( Q p ∧ ¬ p ) (call it $$\eta $$ η ) for the similar possibilitate $$\Diamond \forall q(Qq\!\leftrightarrow \!(\eta \!\leftrightarrow \! q))$$ ◊ ∀ q ( Q q ↔ ( η ↔ q ) ). The attempted disproof of this premise-pair—again, a constructive one—cannot succeed. It cannot be brought into normal form. The criterion says the premise-pair is a genuine paradox. In §4 we show how Russell’s Paradox of Propositions, like the Priorean intensional paradoxes, is to be classified as a genuine paradox by the proof-theoretic criterion of paradoxicality. (shrink)

It has been argued that reduction procedures are closely connected to the question about identity of proofs and that accepting certain reductions would lead to a trivialization of identity of proofs in the sense that every derivation of the same conclusion would have to be identified. In this paper it will be shown that the question, which reductions we accept in our system, is not only important if we see them as generating a theory of proof identity but is also (...) decisive for the more general question whether a proof has meaningful content. There are certain reductions which would not only force us to identify proofs of different arbitrary formulas but which would render derivations in a system allowing them meaningless. To exclude such cases, a minimal criterion is proposed which reductions have to fulfill to be acceptable. (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.

The initial premise of this paper is that the structure of a proof is inherent in the definition of the proof. Side conditions to deal with the discharging of assumptions means that this does not hold for systems of natural deduction, where proofs are given by monotone inductive definitions. We discuss the idea of using higher order definitions and the notion of a functional closure as a foundation to avoid these problems. In order to focus on structural issues we introduce (...) a more abstract perspective, where a structural proof theory becomes part of a more general theory of functional closures. A notion of proof equations is discussed as a structural classifier and we compare the Russell and Ekman paradoxes to illustrate this. (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)

Dag Prawitz (1971) put forward the idea that an admissible reduction process does not affect the identity of proofs represented by derivations in natural deduction. The idea relies on his conjecture that two derivations represent the same proof if and only if they are equivalent in the sense that they are reflexive, transitive and symmetric closure of the immediate reducibility relation. Schroeder-Heister and Tranchini (2017) accept Prawitz’s conjecture and propose the triviality test as the criterion for admissible reductions. In the (...) present paper, we will consider two main troubles of the triviality test. The first is the obscurity of a method of evaluating admissible reductions. The second is the circularity problem that the triviality test already assumes the set of admissible reduction procedures. For the solution of the problems, we will propose the spoiler test which immunes the problems of the triviality test and has the role of the criterion for admissible reductions. At last, we shall cover a plausible problem of the spoiler test that can be caused by Crabbé’s case. (shrink)

A proof-theoretic test for paradoxicality was famously proposed by Tennant: a paradox must yield a closed derivation of absurdity with no normal form. Drawing on the remark that all derivations of a given proposition can be transformed into derivations in normal form of a logically equivalent proposition, we investigate the possibility of paradoxes in normal form. We compare paradoxes à la Tennant and paradoxes in normal form from the viewpoint of the computational interpretation of proofs and from the viewpoint of (...) proof-theoretic semantics. (shrink)

In the present paper, the Fregean conception of proof-theoretic semantics that I developed elsewhere will be revised so as to better reflect the different roles played by open and closed derivations. I will argue that such a conception can deliver a semantic analysis of languages containing paradoxical expressions provided some of its basic tenets are liberalized. In particular, the notion of function underlying the Brouwer–Heyting–Kolmogorov explanation of implication should be understood as admitting functions to be partial. As argued in previous (...) work, the correctness of an inference rule should not be defined in terms of transmission of provability, but rather should be grounded on weaker principles, which I show that are motivated by consideration about the content of the inversion principle. In the conclusion, I briefly address the issue of compositionality, arguing that the violation of compositionality induced by paradoxes are no worse than others that are regarded, at least by Dummett, as wholly unproblematic. (shrink)

For the past 40 years, Neil Tennant has defended a proof-theoretic criterion of self-referential paradoxicality. According to this criterion, the defining characteristic of paradoxes is that, when formulated within a natural deduction system, they produce derivations that cannot be normalized. This paper raises doubts about Tennant’s approach. Recently, Tennant has suggested that Russell’s paradox might not truly fit his criterion. I will argue that the reasoning that rules out Russell’s paradox can similarly be applied to some semantic paradoxes. Therefore, if (...) Tennant’s assessment of Russell’s paradox holds, few cases may genuinely qualify as paradoxes by his standards. (shrink)

Developing early results of Prawitz, Tennant proposed a criterion for an expression to count as a paradox in the framework of Gentzen’s natural deduction: paradoxical expressions give rise to non-normalizing derivations. Two distinct kinds of cases, going back to Crabbé and Tennant, show that the criterion overgenerates, that is, there are derivations which are intuitively non-paradoxical but which fail to normalize. Tennant’s proposed solution consists in reformulating natural deduction elimination rules in general form. Developing intuitions of Ekman we show that (...) the adoption of general rules has the consequence of hiding redundancies within derivations. Once reductions to get rid of the hidden redundancies are devised, it is clear that the adoption of general elimination rules offers no remedy to the overgeneration of the Prawitz–Tennant analysis. In this way, we indirectly provide further support for a solution to one of the two overgeneration cases developed in previous work. (shrink)

In this autobiographical sketch, which is followed by a bibliography of my writings, I try to relate my intellectual development to problems, ideas and results in proof-theoretic semantics on which I have worked and to which I have contributed.