Since the appearance of Prior’s tonk, inferentialists tried to formulate conditions that a collection of inference rules for a logical constant has to satisfy in order to succeed in conferring an acceptable meaning to it. Dummett proposed a pair of conditions, dubbed ‘harmony’ and ‘stability’ that have been cashed out in terms of the existence of certain transformations on natural deduction derivations called reductions and expansions. A long standing open problem for this proposal is posed by quantum disjunction: although its (...) rules are intuitively unstable, they pass the test of existence of expansions. Although most authors view instabilities of this kind as too subtle to be detected by the requirement of existence of expansions, we first discuss a case showing that this requirement can indeed detect instabilities of this kind, and then show how the expansions for disjunction-like connectives have to be reformulated to rule out quantum disjunction. We show how the alternative pattern for expansions can be formulated for connectives and quantifiers whose rules satisfy a scheme originally developed by Prawitz and Schroeder-Heister. Finally we compare our proposal with a recent one due to Jacinto and Read. (shrink)

A first-order language with a defined identity predicate is proposed whose apparatus for atomic predication is sensitive to grammatical categories of natural language. Subatomic natural deduction systems are defined for this naturalistic first-order language. These systems contain subatomic systems which govern the inferential relations which obtain between naturalistic atomic sentences and between their possibly composite components. As a main result it is shown that normal derivations in the defined systems enjoy the subexpression property which subsumes the subformula property with respect (...) to atomic and identity formulae as a special case. The systems admit a proof-theoretic semantics which does not only apply to logically compound but also to atomic and identity formulae—as well as to their components. The potential of the defined systems for a meticulous first-order analysis of natural inferences whose validity crucially depends on expressions of some of the aforementioned categories is demonstrated. (shrink)

This volume is dedicated to Prof. Dag Prawitz and his outstanding contributions to philosophical and mathematical logic. Prawitz's eminent contributions to structural proof theory, or general proof theory, as he calls it, and inference-based meaning theories have been extremely influential in the development of modern proof theory and anti-realistic semantics. In particular, Prawitz is the main author on natural deduction in addition to Gerhard Gentzen, who defined natural deduction in his PhD thesis published in 1934. The book opens with an (...) introductory paper that surveys Prawitz's numerous contributions to proof theory and proof-theoretic semantics and puts his work into a somewhat broader perspective, both historically and systematically. Chapters include either in-depth studies of certain aspects of Dag Prawitz's work or address open research problems that are concerned with core issues in structural proof theory and range from philosophical essays to papers of a mathematical nature. Investigations into the necessity of thought and the theory of grounds and computational justifications as well as an examination of Prawitz's conception of the validity of inferences in the light of three “dogmas of proof-theoretic semantics” are included. More formal papers deal with the constructive behaviour of fragments of classical logic and fragments of the modal logic S4 among other topics. In addition, there are chapters about inversion principles, normalization of proofs, and the notion of proof-theoretic harmony and other areas of a more mathematical persuasion. Dag Prawitz also writes a chapter in which he explains his current views on the epistemic dimension of proofs and addresses the question why some inferences succeed in conferring evidence on their conclusions when applied to premises for which one already possesses evidence. (shrink)

In the recent literature on proof-theoretic semantics, there is mention of a generality condition on defining rules. According to this condition, the schematic formulation of the defining rules must be maximally general, in the sense that no restrictions should be placed on the contexts of these rules. In particular, context variables must always be present in the schematic rules and they should range over arbitrary collections of formulae. I argue against imposing such a condition, by showing that it has undesirable (...) results and that it is ill-supported by the arguments brought in its favour. (shrink)

The concept of “necessity of thought” plays a central role in Dag Prawitz’s essay “Logical Consequence from a Constructivist Point of View” (Prawitz 2005). The theme is later developed in various articles devoted to the notion of valid inference (Prawitz, 2009, forthcoming a, forthcoming b). In section 1 I explain how the notion of necessity of thought emerges from Prawitz’s analysis of logical consequence. I try to expound Prawitz’s views concerning the necessity of thought in sections 2, 3 and 4. (...) In sections 5 and 6 I discuss some problems arising with regard to Prawitz’s views. (shrink)

A logical constant is weakly disharmonious if its elimination rules are weaker than its introduction rules. Substructural weak disharmony is the weak disharmony generated by structural restrictions on the eliminations. I argue that substructural weak disharmony is not a defect of the constants which exhibit it. To the extent that it is problematic, it calls into question the structural properties of the derivability relation. This prompts us to rethink the issue of controlling the structural properties of a logic by means (...) of harmony. I argue that such a control is possible and desirable. Moreover, it is best achieved by global tests of harmony. (shrink)

In a recent paper del Valle-Inclan and Schlöder argue that bilateral calculi call for their own notion of proof-theoretic harmony, distinct from the usual (or ‘unilateral’) ones. They then put forward a specifically bilateral criterion of harmony, and present a harmonious bilateral calculus for classical logic. In this paper, I show how del Valle-Inclan and Schlöder’s criterion of harmony suggests a notion of normal form for bilateral systems, and prove normalisation for two (harmonious) bilateral calculi for classical logic, HB1 and (...) HB2. The resulting normal derivations have the usual desirable features, like the separation and subformula properties. HB1-normal form turns out to be strictly stronger that the notion of normal form proposed by Nils Kürbis, and HB2-normal form is neither stronger nor weaker than a similar proposal by Marcello D’Agostino, Dov Gabbay, and Sanjay Modgyl. (shrink)

Harmony and conservative extension are two criteria proposed to discern between acceptable and unacceptable rules. Despite some interesting works in this field, the exact relation between them is still not clear. In this article, some standard counterexamples to the equivalence between them are summarized, and a recent formulation of the notion of stability is used to express a more refined conjecture about their relation. Then Prawitz's proposal of a counterexample based on the truth predicate to this refined conjecture is shown (...) to rest on dubious assumptions. As a consequence, two new counterexamples are proposed: one uses the extension of logic with a small amount of arithmetic, while the other uses the extension of a small fragment of arithmetic with a problematic operator defined by Peano. It is argued that both these new counterexamples work fine to reject the conjecture and that the last one works also as a rejection of harmony as a complete criterion of acceptability of rules. (shrink)

Theoria, Volume 88, Issue 4, Page 829-849, August 2022.

Proof-theoretic semantics is an inferentialist theory of meaning, usually developed in a multiple-assumption and single-conclusion framework. In that framework, this theory seems unable to justify classical logic, so some authors have proposed a multiple-conclusion reformulation to accomplish this goal. In the first part of this paper, the debate originated by this proposal is briefly exposed and used to defend the diverging opinion that proof-theoretic semantics should always endorse a single-assumption and single-conclusion framework. In order to adopt this approach some of (...) its _criteria_ of validity, especially separability, need to be weakened. This choice is evaluated and defended. The main argument in this direction is based on the circular dependences of meaning between multiple assumptions and conjunctions, and between multiple conclusions and disjunctions. In the second part of this paper, some systems that suit the new requirements are proposed for both intuitionistic and classical logic. A proof that they are valid, according to the weakened _criteria_, is sketched. (shrink)