Logical Metainferentialism

2.1. Harmony in Natural Deduction

Dummett coined and used the term ‘harmony’ in a restrictive sense, to denote a kind of match between the natural deduction introduction and elimination rules for a logical constant that marks it as endowed with a coherent meaning (Dummett 1991). Following Gentzen (1969), he conceives of harmony as a relation between the introduction rules, taken to be self-justified or definitional, and the elimination rules, viewed as needing justification. Harmony obtains when the latter are not stronger than the introductions. The converse direction, ensuring that the eliminations are not weaker than the introductions, is discussed by Dummett under the separate category of stability (see §2.1.2).

Here we use the term in a (not that uncommon) broader sense, denoting the overall balance between introductions and eliminations for a constant c that is required for their success as implicit definitions of c. Thus, we neither prioritise introductions over eliminations (or conversely) nor do we assign a direction to the relation.²

2.1.1. Harmony as Conservativeness

Dummett’s account of harmony draws heavily on Belnap’s earlier solution to Prior’s tonk (Belnap 1964; Prior 1960). Governed by the rules:

tonk is introduced as a disjunction and eliminated as a conjunction. It is readily seen that tonk trivialises set-based, single-conclusion, reflexive, monotonic and transitive consequence relations on formulae (called Tarskian and formally defined in the Appendix, Definition 6):

Since A and B are arbitrary (thus possibly logically complex), this is a non-conservativeness result over the logical vocabulary in which A and B are formulated: tonk generates inferential relations between formulae dominated by connectives other than tonk that cannot in general be established by their introductions and eliminations alone. By the same token, tonk also non-conservatively extends the structural properties of the colon, the symbol we choose to separate the antecedent from the succedent in a sequent. If, e.g., A and B are atoms, then a novel structural property—that any two atomic formulae stand in the ‘:’ relation—can be established using its rules.

Belnap took the failure of conservativeness to amount to a definitional failure in the context of Tarskian consequence relations. Specifically, he noted that:

we can distinguish between the admissibility of the definition of [∧] and the inadmissiblity of [tonk] on the grounds of consistency—i.e., consistency with antecedent assumptions. (Belnap 1964: 131)

‘Admissibility’ is used here in an informal sense and probably the same is true of ‘consistency,’ although tonk leads to triviality and ceteris paribus to inconsistency too. In any case, tonk is clearly incompatible, if not outright inconsistent, with the “antecedent assumptions” regarding deducibility.

Dummett’s use of conservativeness is somewhat different; it wards against creative, not just catastrophic, putative definitions:

when an expression, including a logical constant, is introduced into the language, the rules for its use should determine its meaning, but its introduction should not be allowed to affect the meaning of sentences already in the language. If, by its means, it becomes possible for the first time to derive certain such sentences from other such sentences, then either their meanings have changed or those meanings were not, after all, fully determined by the use made of them. (Dummett 1991: 218)

This is exactly what tonk does, i.e., it steers us in the unacceptable direction of admitting that the meaning of the other constants is not determined fully by their rules.

2.1.3. Harmony: Global and Local

Harmony can be viewed at two different levels: globally, as a feature of the comprehensive system of all the meaning-conferring rules for the constants in the language, or locally, as a relation between the introduction and the elimination rules for a specific constant. Dummett (1991) distinguishes harmony as conservativeness, which he calls “total” harmony and which is a global property, from “intrinsic” harmony, which is a local property. In natural deduction, sequences of rule applications where an introduction is followed immediately by the application of the corresponding elimination, like, e.g.,

are unfocussed or redundant. The formulas that are both conclusions of the introduction and major premisses of the elimination (A ∧ B in the example above) are detours in the proof. Their exhibited consequences are already available

and the detour can be eliminated.

Dummett equates intrinsic harmony with the existence of reductions for these “local peaks.” The reductions (or detour conversions) are one ingredient of normalisation theorems (Prawitz 1965), which require, in general, a further type of conversion permuting the order of the application of the rules (permutation conversions). Needless to say, tonk-generated local peaks are not eliminable, rendering it intrinsically disharmonious as well as non-conservative, i.e., totally disharmonious.

2.2. Harmony in the Sequent Calculus

Dummett’s discussion of harmony is placed within the context of his revisionist attempt to replace the hegemony of classical logic with that of intuitionistic logic. He argues that classical negation is disharmonious because it is non-conservative. There are classically valid, negation-free formulae, such as Peirce’s law, ((A → B)→A)→A, that can only be proved using the rules for negation.

Defenders of classical logic have countered that the problems do not lie with any of its intrinsic features—in particular, nothing is wrong with classical negation—but with the natural deduction format which, while well-designed to accommodate intuitionistic deductions, is a Procrustean bed for the classical ones. Because Gentzen-style natural deduction is single-conclusion, the proofs of some classical implicational laws cannot be obtained in its positive fragment (which is the same as the intuitionistic one).

The problem does not arise in proof systems where multiple conclusions are allowed. Although multiple-conclusion natural deduction systems have been developed (Boričić 1985; Shoesmith and Smiley 1976), this feature is more widely associated with sequent calculi. Indeed, several authors have viewed the sequent calculus as a more appropriate environment to investigate harmony, because it is less biased towards a specific logic than natural deduction (Hacking 1979; Schroeder-Heister 2012b; Wansing 2000). It is claimed that the sequent calculus offers the best of both worlds, as it solves the aforementioned difficulties and encodes natural deduction derivations within its own proofs, under a construal of sequents as claims to the effect that the succedent can be derived in natural deduction from the open assumptions in the antecedent.⁵

Upon switching to the sequent calculus, then, nothing is lost in terms of the pre-existing accomplishments about harmony. The balance between the introduction and the elimination rules for a constant is recast as a balance between its right and left introductions. True, there are thorny questions posed by the presence of structural rules and their role in meaning determination (Dicher 2016a), but these need not detain us right now. It is more important to observe that Identity and Cut are non-negotiable rules from this perspective. Their correctness stems from the interpretation of sequents as abridged natural deduction derivations. By definition, every single-node tree consisting of the open assumption A is a natural deduction derivation of A from A itself. Moreover, natural deduction derivations can be chained by grafting a derivation of a formula A onto any derivation where A is an open assumption.

In this new context, the problem of harmony can again be addressed both locally and globally. Locally, this involves determining when the left and right introduction rules for a given constant c are harmonious. Globally, it involves assessing which sequent calculi are, on the whole, harmonious.

Locally, the reducibility of maximal peaks corresponds to the eliminability of applications of Cut where both occurrences of the Cutformula are principal in the applications of the rules that yield the premisses of Cut—a property sometimes referred to as Cut-inductivity (Humberstone 2020). For example, the Cut-containing proof

reduces to

It is then natural to view calculi that admit Cut elimination as globally harmonious, and to take Cut-free proofs as the sequent calculus incarnations of normal proofs. In Cut elimination algorithms, the complexity-lowering reductions exemplified above (roughly) correspond to detour conversions, while rank-lowering reductions (roughly) correspond to permutation conversions.

The eliminability of Cut is a stronger guarantee of global harmony than normalisability, because it is more intimately connected with conservativeness (Dummett’s mark of “total” harmony). While applications of the operational rules invariably result in formulae being inserted into the conclusion, Cut is usually the only sequent rule that can eliminate a piece of logical vocabulary already present in a proof. Therefore, it is the only rule that can generate proofs of formulae none of which contains some constant c whose rules have been applied in the proof. If Cut is eliminable from a sequent’s proof, then there is a proof of the same sequent that avoids using such “unwitnessed” rules. Thus conservativeness is guaranteed.

3.1. Meaning Determination and Logics

The shift towards the sequent calculus as the main tool of the working inferentialist is salutary. Yet it brings with it some peculiar problems (Dicher and Paoli 2021). Sequent calculus inferentialists are committed to some version of the claim that the meaning of the logical constants is determined by their operational rules. Rules belong to logical calculi, which in themselves are just devices for the syntactic manipulation of formal symbols. Yet calculi are generally viewed as syntactic presentations of logics. What entitles us to say that a sequent calculus C is a calculus for an antecedently defined logic L? Is there a unique consequence relation that can be extracted from, or associated to, C?

This question turns out to be much less straightforward than one may gather from the literature. The problem is either overlooked or mistakenly thought to have an obvious answer, namely, the internal relation of C (Avron 1991), i.e., the relation that obtains between a set of formulas X and a formula A iff C proves the sequent X:A.⁶ This identification is prompted by the view that sequents are “claims of consequence,” stating that the succedent can be derived in natural deduction from the open assumptions in the antecedent. It is further supported by the attendant construal of structural rules as proxies for properties of such a consequence relation—for example, Weakening is a proxy for Monotonicity, and Cut acts as a proxy for Transitivity.

Upon careful reflection, this can be seen to be a hasty generalisation from the intuitionistic and classical calculi. These are pretty much the only calculi where this identification will work. Virtually everywhere else, the internal relation of a calculus is not a consequence relation at all; at least, it is not a Tarskian one. A detailed account of the reasons why this is so can be found in (Dicher and Paoli 2021). In a nutshell, though:

1. Many calculi use sequents whose antecedents are multisets or lists of formulae, not sets. Depending on the available structural rules, an equivalent set-theoretical formulation may not be possible. A Tarskian consequence relation is a relation between a set of formulae and a formula.

2. Tarskian consequence relations are reflexive, monotonic, and transitive. The internal relation of a calculus has these properties only if the required structural rules are present.

3. Sequents need not have the same form as claims of consequence. This is already evident in multiple-conclusion calculi, but the problem is most conspicuous for calculi using more complex syntactic units, like hypersequent or labelled deduction calculi.

Aside from these concerns, associating internal relations with consequence relations relevant for meaning determination is also problematic due to Quine’s well-known critique regarding meaning variance in deviant logics (Quine 1970). To counter Quine’s objections, it is natural for inferentialists to claim that logical constants do not change their meanings across the internal relations of calculi that share the same operational rules (Paoli 2014; Restall 2014). Nonetheless, even under these ideal circumstances, the sequent symbol can be taken to mean different things for each of these calculi—a problem sometimes labelled as A-variance (Hjortland 2013). If the Belnapian antecedent context of deducibility, a prerequisite of meaning determination, does not stay the same, then meaning variance threatens again.

Yet every sequent calculus uniquely determines a derivability relation among sequents.⁷ This relation is reflexive, monotonic, and transitive, and holds between a set of sequents and a sequent. Since meaning-conferring rules regulate transitions among sequents, it is rational to pick this relation as the crucial one in respects relevant to meaning determination. Should one complain that what we get is not a tried and true consequence relation on formulae, note that there is a well-worked theory of equivalence of consequence relations on different syntactic units (e.g., formulae, sequents, equations), due to Blok and Jónsson (2006) that can provide the missing link. (See §6 for a précis.) Although, in a primary sense, the consequence relation that is fundamental for meaning determination is a relation on sequents, in a derivative sense any consequence relation on formulae that is Blok-Jónsson equivalent to it can perform the same function. It may well be impossible to unequivocally associate a pre-existing traditional Tarskian relation L to a given sequent calculus C, but Blok-Jónsson equivalence gives us the means to decide whether C can be regarded as a calculus for L.

Because on the received view sequents codify inferences, and the aforementioned derivability relation holds between sequents, one can call it—in full accord with the established practice—metainferential.

In the remainder of this paper we will develop a version of logical metainferentialism: an account of harmony that benchmarks rules against sequent-to-sequent derivability. Observe that a reconsideration of the central notions of inferentialism along the lines sketched above is not isolated. On the one hand, it is in keeping with some recent trends in proof-theoretic semantics, like Schroeder-Heister’s (2012a) critique of the “priority of the categorical over the hypothetical.” On the other hand, a strong emphasis on the role of metainferences characterises the so-called “Buenos Aires plan” for the construction of semantically closed but nontrivial theories, in primis, of truth, where no classical deductive pattern is abandoned or restricted (Barrio et al. 2021; Pailos and Da Ré 2023). The analogies between such research programmes and ours are partly verbal and partly substantive. Gauging the extent to which they dovetail remains a task for the future.⁸

3.2. An Environment for Metainferential Harmony

How should we re-examine the requirements of local and global harmony once sequent-to-sequent derivability (or, less coyly put, consequence) is the primary milieu for studying meaning-conferring inference rules? Several consequences of this move are immediate.

First, if meaning determination is relative to the sequent-to-sequent derivability relation of a calculus, then harmony and the notion of a normal proof must be revisited with a focus on derivations from assumptions, not on proofs from axioms.

Second, harmony criteria (whether local or global) based on Cut elimination alone are a non-starter. Even in the usual classical or intuitionistic calculi, Cut is eliminable from proofs, but not from derivations. In spite of this, since proofs are a special case of derivations, it is desirable to devise criteria that specialise to the customary Cut elimination-based criteria when we restrict our attention to them.

Third, the structural rules of Identity and Cut lose their non-negotiable status. Since a derivation tree’s leaves can be labelled by assumptions, in addition to axioms, axiom-less (hence theorem-less) sequent calculi become worthy of notice in so far as they may have nontrivial derivability relations. Also, a defence of Cut as a principle that allows chaining together abridged natural deduction derivations as encoded by sequents (Williamson 2018), becomes much less compelling. Nothing prevents the chaining of sequent-to-sequent derivations even in the absence of Cut.

When Identity or Cut are not available, the standard format of sequent calculi is sub-optimal. An example will clarify the foregoing claim. In the calculi for either classical or intuitionistic logic, the sequent A:B is derivable from A:B ∧ C, as the conclusion A:B follows by Cut from A:B ∧ C and B ∧ C:B. In turn, this can be obtained by the left conjunction rule (plus, possibly, some structural rules) from B:B. Without Cut, the final inference is illegitimate, and without Identity, there’s no way to get to B ∧ C:B in the first place.

In other words, without Identity or Cut we need alternative ways to decompose formulae in order to use their subformulae. Elimination rules can achieve this. Thus, the combined provisions of promoting derivations to first-class citizens and giving up the previously inviolable principles of Identity and Cut lead us to adopt hybrid systems that blend features of sequent calculi and natural deduction. These systems contain, alongside the usual left and right introduction rules, less usual left and right elimination rules.

Our subsequent exemplification is based on a family of propositional sequent calculi dubbed (PK⁼)—with the parentheses an integral part of the name. Their language ℒ contains the connectives ¬, ∧, ∨. A (PK⁼) sequent X:Y is an ordered pair of finite multisets of ℒ-formulae. Figure 1 presents the operational rules of (PK⁼); the double line is used to compress notationally both introduction rules (top to bottom) and elimination rules (bottom to top), the left label marks the eliminations, the right one the introductions. Figure 2 presents the structural rules that hold for the entire family, i.e., Weakening and Contraction. Finally, Figure 3 presents the structural rules that make the difference between the calculi in it, namely Cut and Identity (or Id for short).

Figure 1

Operational rules of PK⁼.

Figure 2

Weakening and Contraction.

Figure 3

Id and Cut.

We use PK⁼ without parentheses to label the minimal calculus in the family (PK⁼). It lacks both Cut and Id. Additionally:

• $\mathit{\text{PK}}{=}_{\mathit{\text{df}}}P{K}^{=}\cup \{\mathit{\text{Id}},\mathit{\text{Cut}}\}$;

• $P{K}_{\mathit{\text{Id}}}^{–}{=}_{\mathit{\text{df}}}P{K}^{=}\cup \{\mathit{\text{Id}}\}$;

• $P{K}_{\mathit{\text{Cut}}}^{–}{=}_{\mathit{\text{df}}}P{K}^{=}\cup \{\mathit{\text{Cut}}\}$.

(PK⁼) contains both the usual right and left introductions and their inverses, serving as eliminations.

Definition 1 (Inverse rule). Let Seq(C) be the set of sequents of a Gentzen-style calculus C and let ρ∈C be a rule that applied to $\{S_1,\mathrm{\dots },S_n\}\subseteq \mathit{\text{Seq}}(C)$ yields S∈Seq(C). The rule ρ is inverted by the rules ${\rho }_i^{\iota }(i=1,\mathrm{\dots },n) \text{iff} {\rho }_i^{\iota }$ yields S_i when applied to S, for $i\in \{1,\mathrm{\dots },n\}$.

In PK, the inverses are derivable. In the substructural calculi in the family, this is no longer the case, although they remain admissible (see below).

The following Example gives a flavour of the way these calculi work:

Example 1.

• (1) $:\neg (A\wedge B){⊢}_{P{K}^{=}}:\neg A\vee \neg B$

  

• (2) $:A\vee B,:\neg A{⊢}_{P{K}_{\mathit{\text{Cut}}}^{–}}:B$

  

• (3) $:{⊢}_{P{K}_{\mathit{\text{Id}}}^{–}}:A\vee \neg A$

  

• (4) $:A,:\neg A{⊢}_{\mathit{\text{PK}}}:B$

  

The next proposition characterises the relation between (PK⁼) and the well-known logics in the FDE-family. The results have been proved as follows: (i) is proved in Přenosil (2017); for (ii) see, additionally, Barrio et al. (2015); Dicher and Paoli (2019); Pynko (2010); a proof of (iii) is given in French (2016); Přenosil (2017), while for (iv), see Dicher and Paoli (2019; 2021); Přenosil (2017); Pynko (2010). See also §6, as well as French (2022) for another statement of all these results in bullet list form.

Proposition 1.

• (i)

  ${⊢}_{P{K}^{=}}$ is (Blok-Jónsson similar to) FDE.

• (ii)

  ${⊢}_{P{K}_{\mathit{\text{Id}}}^{–}}$ is (Blok-Jónsson similar to) LP.

• (iii)

  ${⊢}_{P{K}_{\mathit{\text{Cut}}}^{–}}$ is (Blok-Jónsson similar to) K3.

• (iv)

  ⊢_PK is (Blok-Jónsson similar to) classical logic CL.

The subsequent treatment of harmony is indebted to Adam Přenosil’s 2017, to whom many of the following definitions and results, pertaining to sequent calculi in general and (PK⁼) in particular, must be credited.

Definition 2. Let C be a sequent calculus and let Seq(C) be the set of its sequents.

1. A theorem of C is any member of Seq(C) that can be proved in C.

2. An antitheorem of C is any subset of Seq(C) from which the empty sequent can be derived in C.

3. A rule is admissible in C iff its addition to C does not yield new theorems.

4. A rule is antiadmissible in C iff its addition to C does not yield new antitheorems.

Although one cannot help noticing the dualities intrinsic in Definition 2, there is also a certain asymmetry between the concepts of a theorem and of an antitheorem: whereas a theorem is a sequent, an antitheorem is a set of sequents. This is to be expected given that sequent-to-sequent derivability relations are, by design, single-conclusioned—hence properties of sequents based on their respective roles as premisses or conclusions must, to some extent, be lopsided.

We collect in the next proposition a number of useful results about (PK⁼), some of which belong to the folklore—in particular, item (4) can be viewed as a formulation of the Inversion Theorem: see e.g. Buss (1998)—while the rest are proved in Přenosil (2017).

Proposition 2.

1. $P{K}_{\mathit{\text{Id}}}^{–}$ and PK have the same theorems. PK⁼ and $P{K}_{\mathit{\text{Cut}}}^{–}$ have no theorems.

2. $P{K}_{\mathit{\text{Cut}}}^{–}$ and PK have the same antitheorems. PK⁼ and $P{K}_{\mathit{\text{Id}}}^{–}$ have no antitheorems.

3. In PK, the introductions and eliminations for each connective are interderivable.

4. In $P{K}_{\mathit{\text{Id}}}^{–}$ without the eliminations, the eliminations are admissible.

5. In $P{K}_{\mathit{\text{Cut}}}^{–}$ without the introductions, the introductions are antiadmissible.

6. In $P{K}_{\mathit{\text{Id}}}^{–}$ without the eliminations, Cut is admissible.

7. In $P{K}_{\mathit{\text{Cut}}}^{–}$ without the introductions, Id is antiadmissible.

3.3. The Dimensions of Harmony

A satisfactory metainferential account of harmony should encompass both the local and the global dimension. In addition, it should identify appropriate formal requirements that witness each of these dimensions. From a more philosophical perspective, it should characterise the inferential roles of the logical constants that are now typically defined via four (not just two) rules.⁹ In this subsection we will investigate the formal component of local and global harmony. We defer the account of the inferential roles in (PK⁼) to §4.

In standardly interpreted sequent calculi, local harmony amounts to the balance between right- and left-introductions:

$\begin{array}{ccc}\mathit{\text{Li}}\hfill & ⟷& \hfill \mathit{\text{Ri}}\end{array}$

In (PK⁼), there are more relations relevant for harmony. The familiar, horizontal dimension of harmony now coexists with a vertical dimension. Each (left or right) introduction must be harmonious with the corresponding (left or right) elimination. Moreover, right- and left-eliminations too should be balanced:

$\begin{array}{ccc}\mathit{\text{Li}}\hfill & ⟷& \hfill \mathit{\text{Ri}}\\ \updownarrow \hfill & \text{harmony}& \hfill \updownarrow \\ \mathit{\text{Le}}\hfill & ⟷& \hfill \mathit{\text{Re}}\end{array}$

3.3.1. Local Harmony: the Vertical Dimension

In natural deduction, showing that introductions and eliminations are balanced requires a bypass through reducibility. Nevertheless, the most direct way of obtaining it is by building it into the rules themselves, that is, by ensuring that the rules are invertible. This idea can be straightforwardly extended and applied to each pair consisting of a (left or right) introduction and a (left or right) elimination. In bilaterally interpreted calculi like (PK⁼) (cf. infra, §4) we then obtain an aspect of harmony that concerns the relation between introductions and eliminations of the same polarity.

Because the (PK⁼) rules are invertible, neither the introductions nor the eliminations outstrip the meaning imparted by the other upon the logical constant they govern. The rules are vertically harmonious.

Invertibility entails the reducibility of complexity maxima on both the left and the right. For instance, a (schematically represented) left disjunctive local peak

can be eliminated by reducing the derivation to

By the same token, the rules are stable: by invertibility, the eliminations are not weaker than the introductions.¹⁰

3.3.2. Local Harmony: the Horizontal Dimension

Recall from §2.2 that a widely accepted criterion for local harmony between the left and the right rules for a logical constant c in an introduction-only sequent calculus is the eliminability of all applications of Cut where the Cutformula is dominated by c and is principal in the applications of the rules that yield both premisses of the Cut. In such reductions, the left and right introduction rules for c work in tandem to enable the replacement of an application of Cut on a c-dominated Cutformula with Cuts on its immediate subformulae. If no other constant than c is present and we iterate this procedure, we end up with atomic Cuts, operating on propositional variables.

Dually, the left and the right elimination rules for c, if harmonious, will afford the replacement of instances of Id whose principal formula is dominated by c with instances containing its immediate subformulae. Again, if no other constant than c is present and we iterate the procedure, we eventually get to atomic instances of Id.

For reasons that will be better detailed in the following section, we count left/right rules of the same, respectively, introductive or eliminative character as horizontally harmonious iff they allow atomic reductions of the applications of the structural rules. These are transformations of derivations that involve applications of structural rules with principal formulae of arbitrary complexity, converting them into derivations that contain only atomic applications of the structural rules. For instance, the derivations on the right below illustrate atomic reductions for Weakening in relation to disjunction and, respectively, Contraction in relation to negation:

3.3.3. Global Harmony

As a preliminary step towards tackling the more difficult problem of global harmony, as well as the attendant issue of normal form in sequent calculi, we observe that both the reducibility of local peaks and the atomic reducibility of the applications of structural rules are separation properties in the top-down flow of derivations. The former is a separation property between introductions and eliminations, while the latter is a separation property between operational and structural rules.

In a sequent calculus with eliminations, a derivation usually proceeds by first decomposing the formulae occurring in the assumptions via the eliminations; then the sequents thus obtained, containing less complex formulas, are fed as premisses into the introductions. If there is an irreducible local peak, either an introduction has to be applied too early, before the eliminations have done their work, or an elimination has to be applied too late, when the introductions have already taken centre stage. Similarly, an atomically irreducible application of a structural rule signals an incapacity to separate the structural and the operational segments of the derivation.

This suggests a normal form familiar from natural deduction.¹¹ A normal form derivation consists of three parts. The initial part contains eliminations only. It is followed by a part consisting of atomic applications of structural rules. In the final part there are only applications of introductions. The following definitions and results, due to Přenosil (2017), render this informal description precise:

Definition 3.

1. An atomic sequent is a sequent all whose component formulae are atoms.

2. A (PK⁼)-derivation D is structurally atomic if the premisses and the conclusions of all occurrences of structural rules in D are atomic sequents.

3. A (PK⁼)-derivation D is analytic-synthetic iff in each branch of D, all instances of elimination rules precede all instances of introduction rules.

If D is structurally atomic, then D is analytic-synthetic iff no elimination rule in D immediately follows an introduction rule. Hence, structurally atomic analytic-synthetic derivations have the shape described above. A calculus where every derivation can be put in structurally atomic analytic-synthetic normal form (SAAS normal form, for short) has the credentials to be regarded as globally harmonious. This is the case for the (PK⁼) calculi:

Theorem 1 (SAAS normal form). Let $𝖢\in (P{K}^{=})$. If X⊢_CS, then S is C-derivable from X by means of a structurally atomic analytic-synthetic derivation.

An explanation of the term ‘analytic-synthetic’ is in order. One of the most important consequences of Cut elimination in standard sequent calculi is the subformula property. Proofs with the subformula property can be viewed, top-down, as purely synthetic: every formula in them is a subformula of a formula in the endsequent. This is not the case with a generic derivation in SAAS normal form. This will contain a synthetic procedure as its final segment, without, in general, being exhausted by it. There will be an analytic part of the derivation where every formula is a subformula of some formula occurring in an assumption. In more rigorous terms:

Definition 4. A (PK⁼)-derivation D of S from X has the general subformula property iff each formula in D is a subformula of some formula either in X or in S.

Theorem 2. Let $𝖢\in (P{K}^{=})$. If X⊢_CS, then S is C-derivable from X by means of a structurally atomic analytic-synthetic derivation with the general subformula property.

Below, the derivation (a) contains both a local peak and a non-atomic application of Cut. Both can be removed, and the derivation (c) is in SAAS normal form. Observe that its introductive (=synthetic) segment is empty.

(a)

(b)

(c)

To summarise, we propose using the normal form described in Theorem 1 as a criterion for global harmony. The SAAS normal form has two components: structural atomicity and analytic-syntheticity. The former accounts for the horizontal dimension of (local) harmony. The latter relates to the interaction between introductions and eliminations and is closely connected to the more descriptive requirement for invertibility—it accounts for the vertical dimension of (local) harmony. Global harmony is thus a composite of the local harmony properties. However, it is more than their sum.

$\begin{array}{ccc}& \underbrace{\text{global harmony}}& \\ \text{local vertical harmony}\hfill & +& \hfill \text{local horizontal harmony}\\ \text{(analytic-syntheticity)}\hfill & & \hfill \text{(structural atomicity)}\end{array}$

Before we proceed to discuss the inferential roles of the logical constants, we pause for brief comment on structural atomicity.

Theorem 1, through its structural atomicity component, generalises the Cut-elimination theorem. Given that the latter is instrumental in establishing conservativeness, this generalisation can also be viewed as an extended conservativeness result. This approach is akin to Hacking’s 1979 position, which explicitly emphasised the need for the overall conservativeness of the logical vocabulary over structural rules qua proxies for the properties of logical consequence.¹²

Hacking’s particular justification of the demand of structural atomicity, based on preserving the properties of consequence, is closed to us, because (PK⁼)-sequents are not considered claims of consequence. Nevertheless, structural atomicity ensures that the structural proof resources of a proof system do not interfere with the meaning-determining operational rules of its logical vocabulary. Establishing a Cut-elimination result demonstrates a specific form of non-interference by confirming the non-creativity of these operational rules.

On this account of harmony no structural rule has a privileged role. The failure of atomic reducibility (more generally, of SAAS-normalisability) is just as bad irrespective of whether it involves Cut or Weakening or Contraction. This means, inter alia, that the spectrum of pathologies that (putative) logical constants may exhibit increases. We will examine some examples in §5.

4.1. Assertion, denial, and FDE

The second component of the harmony problem mentioned at the beginning of §3.3 concerns the inferential roles of the logical constants. One way of specifying these roles is to explain how the formal properties associated with harmony, as discussed in the previous section, have genuine meaning-theoretic significance. With an eye to setting a benchmark, we start again by revisiting the orthodox account.

In a natural deduction framework, the introduction rules for c exhibit the conditions under which we can legitimately assert a formula containing c, while the eliminations specify the consequences we can legitimately draw from an assertion of the same formula. Historically, this picture is closely tied with the early inferentialists’ attempt to replace the metaphysically loaded notion of consequence as truth preservation with a constructively more acceptable concept of preservation of warranted assertability or, in mathematical contexts, of provability.

At least two independent traditions have maintained that this assertion-centred perspective is lopsided. In the pioneering work of Grzegorczyk (1964), which branches into more recent contributions by Shramko and Wansing (2012; 2017), one can find a constructive account of logic where proofs and disproofs are viewed as basic procedures on a par with each other. On the other hand, the bilateralist tradition (Restall 2005; Ripley 2015; Rumfitt 2000; Smiley 1996), although it overlaps only partially with the inferentialist enterprise, advocates a treatment of denial as a primitive speech act that is not reducible to the assertion of a negation.

FDE and its extensions were devised and investigated, by and large, in full extraneity to either perspective. These logics are typically given a truth-conditional semantics or, at best, an informational one, like in Belnap’s interpretation of FDE’s four values as combinations of the epistemic values “told true” and “told false” (Belnap 1977). Despite this, there is an interpretation of FDE as an appropriate logic for deductive reasoning in situations where sentences can be accepted and rejected at the same time (Paoli 2019). Following this suggestion commits us to jettisoning the so-called pragmatic consistency assumption (Mares 2014), according to which it is impossible to (rationally) assert and deny the same sentence at the same time. This is a widely held hypothesis, accepted even by dialetheists (Priest 2006; 2005: 98–99), who are satisfied with the weaker claim that it is sometimes possible to (rationally) assert a sentence and its negation. However, some textual evidence in Belnap’s papers (for which see again Paoli 2019) can be taken as a hint that it was not the latter thesis, but a refusal of the pragmatic consistency assumption, that he has had in mind.

Setting aside these exegetical issues, let us observe that it is possible to consider two different—and, crucially, non-equivalent—bilateralist construals of a PK⁼-sequent X:Y. One could interpret it as a claim to the effect that either some formula in X is warrantedly denied or some formula in Y is warrantedly asserted. Alternatively, X:Y could be read as a claim to the effect that it is not the case that all the formulae in X are warrantedly asserted and all the formulae in Y are warrantedly denied. We call these the positive and the negative construal of that sequent, respectively.

If we maintain that asserting A is not tantamount to failing to deny A, and vice versa, the positive and the negative construal are sensibly kept apart. We do not want to bind too tightly the reflections that follow to an openly bilateralist perspective. Therefore, if one is inclined to replace the assertion/denial talk with other constructively admissible readings, one is free to do so. For the positive construal, some viable options would be: either some formula in X has been refuted or some formula in Y has been proved; either we have conclusive evidence against some formula in X, or we have conclusive evidence for some formula in Y.

Both construals have interesting connections with Dunn’s semantics of relational valuations for FDE (see e.g. Priest 2002: §4.6), which, in their incarnations as tetravaluations (French 2022; French and Ripley 2019) or dual valuations (Fjellstad 2017; 2020), have already appeared in the literature as interpretation devices for proof systems for FDE and its extensions. We first define this concept.

Definition 5. A relational valuation for ℒ is a function v from the set of ℒ-propositional variables to the powerset 𝒫({t, f}) of the set {t, f} of classical values that is inductively extended to non-atomic formulas as follows:

1. $t\in v(\neg A)⟺f\in v(A)$;

2. $f\in v(\neg A)⟺t\in v(A)$;

3. $t\in v(A\wedge B)⟺t\in v(A) \mathit{\text{and}} t\in v(B)$;

4. $f\in v(A\wedge B)⟺f\in v(A) \mathit{\text{or}} f\in v(B)$;

5. $t\in v(A\vee B)⟺t\in v(A) \mathit{\text{or}} t\in v(B)$;

6. $f\in v(A\vee B)⟺f\in v(A) \mathit{\text{and}} f\in v(B)$.

Following French and Ripley (2019), we say that a sequent X:Y has a counterexample if there is a relational valuation w such that t∈w(A) for all A∈X and f∈w(B) for all B∈Y. If we read ‘t∈w(A)’ as ‘A is warrantedly asserted’ and ‘f∈w(A)’ as ‘A is warrantedly denied,’ the negative construal of a sequent X:Y pins down what conditions must be in place for that sequent to not have any counterexample. If a sequent has any counterxample, there is a procedure that yields what French and Ripley (2019) calls the exact counterexample to that sequent. To each PK⁼-sequent X:Y one associates a function v from the set of ℒ-formulas to 𝒫({t, f}), according to the stipulations that t∈v(A) iff A∈X, while f∈v(A) iff A∈Y. Applying the PK⁼-rules, one can inductively show that v respects the clauses in Definition 5 and thus is uniquely determined by a relational valuation.

The positive construal is intimately tied to relational valuations, too. If we trade in once more ‘A is warrantedly asserted’ for its semantical counterpart ‘t∈w(A),’ as well as ‘A is warrantedly denied’ for ‘f∈w(A),’ the positive construal of X:Y turns into a constraint on the class of relational valuations that satisfy X:Y. It is this construal that we will keep in mind in the considerations that follow. To state and analyse the individual contributions of each operational or structural rule of PK⁼ to the inferential role of the connectives, we will sample the PK⁼-rules against the backdrop of this interpretation. In so doing, we will freely move between the perspectives of relational valuations and of warranted assertion and denial.

Before we come to that, however, we pause to observe the following about the two structural rules that do not hold in PK⁼, Id and Cut. Id can be informally read as a claim to the effect that every formula is either warrantedly asserted or warrantedly denied. It disallows gaps, and corresponds to the condition that for all v’s and all A’s, either f∈v(A) or t∈v(A). It bars valuations from assigning a formula the empty set, a possibility countenanced by Definition 5. Dually, Cut informally reads as the claim that no formula can be warrantedly asserted and warrantedly denied at the same time. It disallows gluts, and corresponds to the condition that for all v’s and all A’s, not both f∈v(A) and t∈v(A). It bars valuations from assigning a formula the set {t, f}, a possibility also countenanced by Definition 5.

How about the rules for the logical connectives? For negation, the right introduction rule converts an entitlement to deny A into an entitlement to assert ¬A, while its inverse converts an entitlement to assert ¬A into an entitlement to deny A. These two rules correspond, respectively, to the right-to-left and to the left-to-right direction of condition (1) in Definition 5. The left introduction rule converts an entitlement to assert A into an entitlement to deny ¬A, while its inverse converts an entitlement to deny ¬A into an entitlement to assert A. These two rules correspond, respectively, to the right-to-left and to the left-to-right direction of condition (2) in Definition 5.

The right introduction rule for conjunction converts an entitlement to assert both A and B into an entitlement to assert A ∧ B, while its inverses convert an entitlement to assert A ∧ B into entitlements to assert A and to assert B. They correspond to the two directions of condition (3) in Definition 5. The left introduction rule converts an entitlement to deny A (or to deny B) into an entitlement to deny A ∧ B, while its inverse converts an entitlement to deny A ∧ B into an entitlement to deny either A or B. And so we have both directions of condition (4) in Definition 5. The case of disjunction is dual.

4.2. Inferential Roles and Harmony

As the preceding discussion shows, in calculi like PK⁼ the inferential role of a logical constant c has four components, and the four rules for c split the bill equally in taking care of them:

1. The right introduction rule specifies the conditions under which we are entitled to assert a sentence dominated by c.

2. The left introduction rule specifies the conditions under which we are entitled to deny a sentence dominated by c.

3. The right elimination rule specifies the consequences we are entitled to draw from the assertion of a sentence dominated by c.

4. Finally, the left elimination rule specifies the consequences we are entitled to draw from the denial of a sentence dominated by c.

Thus, at the local level, horizontal harmony can be viewed as a demand that there should be a match between the conditions under which are we entitled to an assertion and to a denial of a sentence dominated by c, as well as a demand that there should be a match between the consequences we are entitled to draw from an assertion or denial of a sentence dominated by c. In turn, vertical harmony appears as a demand that there should be a match between the conditions under which are we entitled to assert or deny a sentence dominated by c and the consequences we are entitled to draw from such an assertion or denial.

4.3. Addendum: Metainferential Harmony and Bilateralism at Large

Our interpretation of PK⁼ is distinct from but reminiscent of bilateralist interpretations of either sequent calculi or natural deduction for (generally but not exclusively) classical logic (Francez 2014; Restall 2005; 2013; Rumfitt 2000). It could be useful to underscore some of those differences that are particularly pertinent to the harmony issue.

As noted in §2.1.5 there are prima facie compelling general reasons to prefer a local measure of horizontal harmony. While we do not believe that these are ultimately tenable, it is worth underscoring the fact that extant local bilateralist accounts of harmony are problematic for us, independently of any general considerations.

To flesh things out, focus on the left/right introductions for disjunction:

The left introduction converts the warranted denial of A in X:Y and the warranted denial of B in X:Y into a warrant to deny A ∨ B in X:Y. We need a way to determine whether the right introduction, codifying the conditions for warrantedly asserting A ∨ B in X:Y, is harmonious, given the left introduction (and conversely).

Producing a local account of harmony could start with garden variety reasoning about assertion and denial that could then be appropriately generalised considering the morphology of the rules.¹³ This would yield a sequent calculus counterpart of harmony in form.

With respect to the rules for disjunction, one may reason as follows: The denial of a disjunction in a sequent is warranted if and only if the denial of both disjuncts is warranted in that sequent. Contrapositively, if a disjunction is not warrantedly deniable, then at least one of the conditions warranting its denial must fail. The failure to deny a sentence is tantamount to successfully asserting it. So the assertion of either disjunct in X:Y, i.e., X: Y, A, B suffices for producing the sequent X: Y, A ∨ B, i.e., for the warranted assertion of A ∨ B in X:Y. However, here one presupposes a connection between assertion and denial that need not obtain in PK⁼. As already observed, the failure to deny (assert) a statement is not an automatic license to assert (deny) it. This “procedure” may work when assertion and denial are exclusive and exhaustive but it breaks down if they are not.¹⁴

There are also significant methodological worries. First, the appeal—implicit or explicit—to principles relating assertions and denials would belie the locality of the account as long as we agree that these need not be simply encoded in the mere definition of (PK⁼) as indeed they are not.

Second, even if that were not a worry, it is not clear that an account of harmony can proceed by presupposing generic principles governing assertion and denial. On the view espoused here, these principles are sui generis, pertaining to the nature of the sequents themselves, not to the meaning of the logical operations. This is consistent with acknowledging that any account of harmony will (likely) need to grapple with the interplay between assertion and denial.

How should a theory of harmony, looked at from the perspective of the locality vs. globality debate, handle this interplay? Is it enough to justify an account of harmony that tells of this interaction? We submit that the answer to this question must be affirmative. In pairs of left/right introduction and elimination rules interpreted as in §4.1 we deal with drawing inferences from denied sentences and asserted sentences. The harmony of these rules is, eo ipso, a measure of the way in which assertions and denials interact.

If, contra Read (2000), we expect harmony to rule out some pathological behaviours, then the operational rules defining logical constants must be compatible with the sui generis proof resources of a proof system. This is a direct consequence of pathological behaviours depending on both, as tonk’s case illustrates.¹⁵

Overall, far from being entitled to assume specific properties of sequents when setting up criteria of harmony, we need a notion of harmony that accounts for their interaction with the logical vocabulary. This goes a long way towards vindicating the appeal of a global account of harmony.

We add to this the following remark about locality both in the name of horizontal (and vertical) harmony, and, more importantly, as a constraint on harmony.¹⁶ Horizontal (local) harmony amounts to structural atomicity, the obtaining of which is a function of the structural rules of the calculus. This means that it is not at all a local property, i.e., a property that depends only on the left/right operational rules for the connectives. (However, we continue to call it “local,” because it does not account for every component of harmony.) To be sure, there are good reasons to doubt the plausibility of a purely local criterion for any kind of harmony, horizontal or vertical alike.¹⁷

5.1. Tonk

Recall the sequent calculus rules for tonk:

We can trivially design inverses of these rules to act as eliminations:

Given the non-pathological design of the eliminations with respect to the introductions, tonk fares well as far as the reducibility of complexity maxima is concerned. For instance, those on the right, looking like:

reduce to

The left side case is similar. This ensures that tonk is vertically harmonious in all the systems in (PK⁼). However, this only indicates that the eliminations presented do not replicate the pathology expressed by its natural deduction introduction and elimination.

This may be somewhat unsettling. Yet the reducibility of complexity maxima (which in the case of tonk is tantamount to the invertibility of its rules) is not a vacuous condition: bad behaviour ensues out of rules that fail to satisfy it. Consider tonk⁺ (Humberstone 2020), defined by the rules tonk⁺Ri1= tonkRi1, tonk⁺Re1=tonkRe1, tonk⁺Li1=tonkLi1, tonk⁺Le1=tonkLe1 together with the rules:

Hic sunt dracones, because tonk⁺Ri1 and tonk⁺Re2 suffice to generate irreducible maxima on the right and tonk⁺Li2 and tonk⁺Le1 suffice to generate them on the left:

So tonk⁺ lacks local vertical harmony in every proof system under consideration here.

This boils down to tonk⁺’s introductions being no longer invertible, even though they are the inverses of the corresponding eliminations. Because there are two distinct methods for deriving a tonk⁺-sequent using its introductions, the availability of such a sequent merely guarantees that at least one method for obtaining it must be recoverable. There is no assurance that this is the required one.

The failure of local vertical harmony brings with it the failure of global harmony. Its vertical disharmony generates non-conservativeness even in the absence of Id and Cut. One can use tonk⁺ to derive, e.g., [:B] from $[:A\vee B]$ and [$:\neg A$] in PK⁼:

which is a non-conservativeness result. At the same time, the derivation above, even if assumed, without loss of generality, to be structurally atomic (that is, even if we assume that A and B are atoms), is not in SAAS-normal form as it is not analytic-synthetic.

(A similar diagnosis holds of a ‘tonk^∗’ that mimics in the sequent calculus its elimination-behaviour in natural deduction. Thus, instead of eliminating Atonk^∗B on the right by the inverse of its introductions, we could have picked as elimination rule the projection of the second tonk^∗-junct, thus producing $X:Y,B$ out of $X:Y,A\mathit{\text{ton}}{k}^{\ast }B$. This is clearly non-normalisable because non-invertible.)

Invertibility, while generating local vertical harmony, provides no general guarantee that the L/R rules do not generate aberrant behaviours. Indeed, tonk does “misbehave” if assertion and denial are taken to be exhaustive and exclusive. Clearly, it is non-conservative in the presence of Cut. When Id is present, non-conservativeness is generated by the eliminations. If AtonkB:AtonkB is an axiom, then using the eliminations we obtain the sequent B:A, for any A and B, from the empty set of premisses (= as a theorem). In other words, tonk lacks horizontal harmony in all three systems that extend PK⁼. (See the derivations below, in the discussion of global harmony.)

Two observations are in order. First, the exact nature of the problematic interaction between tonk and the exclusivity and exhaustivity of assertion and denial is yet to be elucidated. If ‘:’ were to stand for consequence, then it is clearly deleterious. As it does not so stand, the nature of the pathology—if that it is—exhibited is less clear. However—and this is the second observation—the one thing that we already know with certainty is that the source of whatever problem we have encountered here lies elsewhere than in the combination of introductions and eliminations.¹⁸

As far as global harmony is concerned, the reader can easily verify that tonk’s behaviour raises no problems in interaction with Contraction or Weakening. It is also plain that tonk fails structural atomicity in the presence of Cut, i.e., in PK or $P{K}_{\mathit{\text{Cut}}}^{–}$. A principal Cut on a tonk-formula

cannot be replaced with cuts on its subformulae and ultimately it cannot be replaced with atomic cuts (which are redundant in the case of PK and the empty set of premisses).

Likewise, tonk does not admit the elimination of Id.¹⁹ There is no way to replace AtonkB:AtonkB with atomic instances of Id because instances of Id for tonk compounds cannot be derived from instances of Id for the tonkjuncts, as an inverted proof search shows:

Since atomic structurality is a component of SAAS-normal form, it follows that tonk is globally disharmonious in any (PK)⁼ calculus which contains Id or Cut.

There is another aspect of the badness of tonk in an Id-free calculus that needs to be pointed out. Take the “inverse” of the previous proof:

It shows that B:A follows from the assumption that AtonkB:AtonkB, which is a somewhat bizarre but hardly problematic result. In $P{K}_{\mathit{\text{Cut}}}^{–}$, we could extend this proof as follows:

This shows that our assumptions have led us astray: the set $\{\mathit{\text{Atonk}}B:\mathit{\text{Atonk}}B,:B,A:\}$ is an antitheorem of $P{K}_{\mathit{\text{Cut}}}^{–}$. This is in line with the meaning-theoretic characterisation of Cut. While it mandates the exclusivity of assertion and denial, our assumptions jointly commit us to both deny and assert both A and B. However, if we were to add Id (=the exhaustivity of assertion and denial) to our proof resources, so that the proof above would proceed from the axiom $\overline{A\mathit{\text{tonk}}B:A\mathit{\text{tonk}}B}$ then the result would have a different significance. In that case, $\{:B,A:\}$ would become a novel antitheorem of PK (cf. Definition 2). That is, Id would not be antiadmissible in it.²⁰

Thus, a more fine-grained analysis of tonk’s shortcomings exhibits the relative deficiency of both its introductions and eliminations. Whereas its introductions render Cut not admissible, its eliminations render Id not antiadmissible.

Unlike tonk, tonk⁺ is compatible with Id: tonk⁺ instances of Id can be replaced by atomic instances of Id (Humberstone 2020). Atonk⁺B:Atonk⁺B can be easily replaced by the derivation:

If it were to be appraised for harmony in a proof system that has no structural resources other than Id, then it would count as horizontal harmonious.

However, that does not render tonk⁺ acceptable tout court in Id-comprising proof systems. Consider the following analytic-synthetic but not structurally atomic “proof”:

If we were to attempt to reduce it to a structurally atomic proof we could obtain the (possibly intermediate) reduct:

which is still not analytic-synthetic and so not in SAAS-normal form. In tonk⁺’s case, the process of structural reduction (local horizontal harmony) introduces ineliminable complexity maxima (local vertical disharmony) and blocks the normalisation process. We leave it to the reader to check that this connective’s interaction with Id and Cut is just as catastrophic as that of its lesser cousin, tonk. (Notice that the proof used to discuss the deficiency of tonk’s eliminations from the perspective of Id can be rewritten, salva congruitate, with tonk⁺ instead of tonk.)

5.2. The Strange Case of Knot

Another putative connective usually taken to be disharmonious is tonk’s dual, knot (Došen and Schroeder-Heister 1985; Humberstone 2020). This is L-introduced as a disjunction and R-introduced as a conjunction, while being eliminated by the inverse rules (the same labelling conventions as in Figure 1 apply):

Traditional proof-theoretic medicine focusses on its introductions and records knot’s pathology as one of deficit, rather than excess. While its introductions interact well with Cut and do not generate non-conservativeness—for instance, the proof

reduces to

nevertheless, knotLi does not fully exploit the inferential license expressed by knotRi. The sequent AknotB:AknotB cannot be derived from axiomatic sequents for its subformulae by applying knot’s introduction rules, as an inverted proof search shows:

In other words, instances of Id over knot-formulae cannot be replaced with atomic instances of Id. Thus knot, no less than tonk, disturbs the anti-admissibility of Id and is horizontally disharmonious in proof systems containing Id. This result is preserved when the eliminations are added.

Yet the addition of the elimination rules in the picture leads to a curious result. First notice that knot is vertically harmonious: complexity maxima can be easily eliminated. Yet the eliminations alone suffice to generate non-conservativeness in the presence of Id. The proof

in PK⁼ merely shows that if one assumes that one has warrant to either deny or assert AknotB, then one has warrant to deny A or assert B, for any A, B. In $P{K}_{\mathit{\text{Id}}}^{–}$, where the top leaf of the derivation would be an axiom, this becomes a non-conservativeness result. Arbitrary denials are coherent with arbitrary assertions. This has immediate and deleterious effects on the meaning of the connectives. For instance, with an application of ¬Ri followed by an application of ∨Ri to A:B we get $[:\neg A\vee B]$; that is, $[:\neg A\vee B]$ is a theorem of $P{K}_{\mathit{\text{Id}}}^{–}$ or it is always coherent to assert $[:\neg A\vee B]$. But this is not something that can be obtained in $P{K}_{\mathit{\text{Id}}}^{–}$ without using knot’s rules. Thus knot, despite being governed by invertible rules, non-conservatively extends the consequence relation of $P{K}_{\mathit{\text{Id}}}^{–}$.

See Table 1 for a systematic summary of these results.

5.3. The Bullet

Our final example, the infamous “bullet” defined by the sequent calculus introductions and eliminations

is a (garrulous) Liar in that $\bullet ⊣⊢\neg \bullet$ (Read 2000).²¹ The point of ∙ was to show that harmony, understood as invertibility within a Tarskian consequence relation given by a natural deduction proof system, does not entail conservativeness. That much is plain both in natural deduction and in the more general type of proof systems considered here. Its rules are invertible, yet it is a trivialising connective for Tarskian consequence relations.

But in (PK⁼), (vertical) invertibility is not all there is to harmony. The bullet fares just as bad if the sequents have all the Tarskian (or Scott)²² properties as it renders Cut not admissible and Id not anti-admissible. So it is globally disharmonious in PK. By now, there is nothing surprising about this verdict.

For the other calculi in the family, the matter of the bullet’s harmony is less straightforward, even if it does not generate triviality or non-conservativeness results. To determine whether it is harmonious or not we must examine its interaction with Id, Contraction and Weakening. Of particular importance is the matter of its horizontal harmony.

Now, one may wonder if the result of such an examination isn’t a foregone conclusion. The bullet is a 0-ary connective. As such, it satisfies the elimination theorems required for SAAS-normalisability, and in particular for structural atomicity, ab initio. It would seem that a favourable judgement with respect to its horizontal harmony is all but guaranteed. At this point it might be sensible to bring up a distinction made in Schroeder-Heister (2016b) between two kinds of “simplicity,” or, less metaphorically, two kinds of atoms. A syntactic atom is an expression of arity 0, a semantic atom is a an expression devoid of specific introduction and elimination rules. The bullet is syntactically atomic but semantically non-atomic. We posit that structural atomicity for semantically non-atomic expressions cannot be vacuous. If we were to allow for the condition to be vacuously satisfied, then we would be allowing for instances in which it generates no constraints on proofs. But the very point of the condition is to constrain proofs. There is nothing ad hoc about insisting on genuine constraints, as the means to discern them are available for semantically non-atomic expressions.

Recall that in standard sequent calculi, Cut elimination results are to be understood quite literally. Applications of Cut to atoms at the leaves of a proof are redundant, because they will produce the same identity sequents as the ones to which Cut was applied. Having no applications of Cut is the ultimate guarantee that none of its applications comes before the application of an elimination rule, as SAAS-normal form prescribes.

Reductions of cuts over bullet in the derivation of the empty sequent from (two instances of) identities over it bring us no closer to this normality desideratum. The successive permutations of the applications of Cut with the other rules will yield the initial derivation. Start with

If we push the Cut up one step on both branches of the initial derivation, we obtain:

A further reduction of, e.g., the rhs of this derivation yields

which further reduced gives us a Cut on identities that yields, obviously, an identity. If we dispense with this Cut we get exactly where we started. A bibliographical aside: This looping behaviour of paradoxical expressions has been already noticed in Prawitz (1965) and Tennant (1982). The central role of Contraction in generating loops, which we will discuss presently, has been mentioned in, e.g., Tranchini (2015). The overall connection between Contraction and the paradoxes was already highlighted in Fitch (1936), while, more recently, Zardini (2019) has advanced a solution to the paradoxes that rests on a rejection of Contraction.

However, the loops can be blocked by dropping Contraction. In that case, the Cut would simply confirm what the axioms are telling us:

and would be eliminable. The derivation above reduces to

The obvious question to ask now is whether there is anything peculiar about the interaction between the bullet and Contraction.

Consider therefore, again, the problem of reductions over 0-adic connectives, this time in the particular case of the bullet and Contraction. If the inference from $\bullet ,\bullet ,X:Y$ to $\bullet ,X:Y$ occurs in an arbitrary proof, does an attempt at a reduction even make sense? In a sense, it does not: the bullet has no proper constituents so there’s nothing to reduce. Yet the premiss could have been obtained via an application of an introduction rule (for the bullet) and the conclusion could be the premiss of an application of a corresponding elimination rule. From a “semantic” perspective, such a derivation provides opportunities for reductions.

The standard reduction procedure involves applying as many eliminations as possible and then contracting the result as needed to reconstitute the eliminated formula by an application of the appropriate introduction. In the case of ∙ there is no end of possible applications of its elimination rules. Suppose that we attempt to systematically apply all the possible left eliminations first, followed by all possible right eliminations, for instance in the proof:

We simply get back where we began:²³

Of course, we could decide to break the chain. We could be satisfied with applying one elimination to each contracted formula and declare it “exhausted” for further applications. Then we could contract on ∙ in $X:Y,\bullet ,\bullet$ and obtain the desired conclusion with a further application of ∙Li. But this is “normalisation by decree,” which alone makes the difference between an application of ∙Li and ∙Re. (Notice that $\top ,\perp$ and λ all admit unequivocal reductions, i.e., reductions in which there is a sequent such that no elimination rule can be applied to it, as opposed to, say, “need not” be applied. So this has nothing to do with the bullet’s arity.)

Were it not for the convenient labelling, a proof of the kind described above would not be reduced. The labels, however, are not part of the proof: they are the expression of the immeasurable lengths some authors go to make life easier for their readers (referees and editors included). If this paper had been written by less accommodating authors, no one could fault a reader who, absent the labels, would conclude that the proof above still needs reduction, as its last step contains an application of an elimination rule that is preceded by a Contraction. Then, instead of contracting, we would have applied ∙Re twice, whereby we would be in the position of contracting ∙ subformulae and then applying ∙Ri once to obtain the desired conclusion. But, for all we know, this last application of an introduction on the right could have been an application of an elimination on the left. And so on, and on, and on, ….

The same holds for Weakening; the proof fragment

reduces in the first instance to

but a decree is again required to consecrate this as a genuine reduct.

This means that the bullet’s rules are such that a proof containing their applications cannot contain a genuine middle-segment, i.e., one in which not only is it the case that no operational rules are applied but in which no elimination rules can be applied. For connectives like the bullet, it is always possible to intersperse a sequence of atomic applications of the structural rules with operational rules without disrupting the atomicity of the entire segment. This is, to say the least, a counterintuitive phenomenon. As an anonymous referee pointed out, this may justify a modification of the requirement for horizontal harmony, specifically to handle cases of the kind described above. While such a modification would be ad hoc, there would be little reason to object, as the bullet itself is an ad hoc creation designed to showcase the limits of conservativeness in Tarskian consequence relations.

The upshot is that, at least on a semantic understanding of atomicity, the bullet is not only bad if Cut and Id are allowed. It is bad in relation to Weakening and Contraction too. Indeed, it is bad in itself. Moreover, its badness doesn’t have much to do with its paradoxicality. Instead, it ensues from a defect of its defining rules. Indeed, this defect is a kind of non well-foundedness phenomenon, yet it is to be distinguished from mere paradoxicality.