According to logical inferentialists, the meanings of logical expressions are fully determined by the rules for their correct use. Two key proof-theoretic requirements on admissible logical rules, harmony and separability, directly stem from this thesis—requirements, however, that standard single-conclusion and assertion-based formalizations of classical logic provably fail to satisfy :1035–1051, 2011). On the plausible assumption that our logical practice is both single-conclusion and assertion-based, it seemingly follows that classical logic, unlike intuitionistic logic, can’t be accounted for in inferentialist terms. In (...) this paper, I challenge orthodoxy and introduce an assertion-based and single-conclusion formalization of classical propositional logic that is both harmonious and separable. In the framework I propose, classicality emerges as a structural feature of the logic. (shrink)

This paper concentrates on how to capture harmony in sequent calculi. It starts by considering a proposal made by Tennant and some objections to it which have been presented by Steinberger. Then it proposes a different analysis which makes use of a double-line presentation of sequent calculi in the style of Dosen and it shows that this proposal is able to dismiss disharmonious operators without thereby adopting any global criterion.

This paper responds to recent work in the philosophy of Homotopy Type Theory by James Ladyman and Stuart Presnell. They consider one of the rules for identity, path induction, and justify it along ‘pre-mathematical’ lines. I give an alternate justification based on the philosophical framework of inferentialism. Accordingly, I construct a notion of harmony that allows the inferentialist to say when a connective or concept is meaning-bearing and this conception unifies most of the prominent conceptions of harmony through category theory. (...) This categorical harmony is stated in terms of adjoints and says that any concept definable by iterated adjoints from general categorical operations is harmonious. Moreover, it has been shown that identity in a categorical setting is determined by an adjoint in the relevant way. Furthermore, path induction as a rule comes from this definition. Thus we arrive at an account of how path induction, as a rule of inference governing identity, can be justified on mathematically motivated grounds. (shrink)

The notion of harmony has played a pivotal role in a number of debates in the philosophy of logic. Yet there is little agreement as to how the requirement of harmony should be spelled out in detail or even what purpose it is to serve. Most, if not all, conceptions of harmony can already be found in Michael Dummett's seminal discussion of the matter in The Logical Basis of Metaphysics. Hence, if we wish to gain a better understanding of the (...) notion of harmony, we do well to start here. Unfortunately, however, Dummett's discussion is not always easy to follow. The following is an attempt to disentangle the main strands of Dummett's treatment of harmony. The different variants of harmony as well as their interrelations are clarified and their individual shortcomings qua interpretations of harmony are demonstrated. Though no attempt is made to give a detailed alternative account of harmony here, it is hoped that our discussion will lay the ground for an adequate rigorous treatment of this central notion. (shrink)

Data involving epistemic modals suggest that some classically valid argument forms, such as _reductio_, are invalid in natural language reasoning as they lead to modal collapses. We adduce further data showing that the classical argument forms governing the existential quantifier are similarly defective, as they lead to a _de re–de dicto_ collapse. We observe a similar problem for disjunction. But if the classical argument forms for negation, disjunction and existential quantification are invalid, what are the correct forms that govern the (...) use of these items? Our diagnosis is that epistemic modals interfere with hypothetical reasoning. We present a modal first-order logic and model theory that characterizes hypothetical reasoning with epistemic modals in a principled manner. One upshot is a sound and complete natural deduction system for reasoning with epistemic modals in first-order logic. (shrink)

In my Steinberger 2009 I argued that Neil Tennant’s Harmony requirement is untenable because of its failure to account for the standard quantifier rules.1 Instead of justifying the customary rules for the existential and universal quantifiers, Tennant’s account appears to sanction only wholly unrestricted – and so patently disharmonious – quantifier rules. In his characteristically thoughtful response Tennant 2010, Tennant offers a sequent calculus version of his Harmony requirement that rules out such pathological would-be quantifiers. While I agree with Tennant (...) that recasting his Harmony requirement in the sequent format as he proposes blocks the said disharmonious quantifier rules, I submit that Tennant’s revamped Harmony requirement nevertheless misses the mark. I present two objections to substantiate my claim. First, I show that the crucial additional assumption underlying Tennant’s sequent calculus-based account – what I call the admissibility assumption – is excessively strong: so strong, in fact, that it renders otiose the core of Tennant’s original account. Second, I argue that the admissibility assumption, as a global requirement on deductive systems, is ill-suited for the purposes of codifying the intuitive notion of harmony. Fortunately, though, as I will demonstrate, we can dispense with the admissibility assumption altogether. (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)

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

The requirement of proof-theoretic harmony has played a pivotal role in a number of debates in the philosophy of logic. Different authors have attempted to precisify the notion in different ways. Among these, three proposals have been prominent in the literature: harmony–as–conservative extension, harmony–as–leveling procedure, and Tennant’s harmony–as–deductive equilibrium. In this paper I propose to clarify the logical relationships between these accounts. In particular, I demonstrate that what I call the equivalence conjecture —that these three notions essentially come to the (...) same thing—is erroneous. (shrink)