On inferential rules for a strange connective

Ever since Prior's tonk it's been a standard logician's parlor game to come up with deviant connectives, undermining the inferentialist project. The trick is to come up with seemingly "nonsensical" operators (e.g., trivializing, inconsistent, etc) which are harmonious, leaving aside for now precisely how to cash out the constraint. I put quotations around 'nonsensical' just to flag that this is a point of contention. Some, like former Archean Roy Cook, has argued that tonk isn't all bad. In particular, it is non-trivalizing if the antecedent logic has restricted transitivity. But, nonetheless, the literature has been ever increasing with new tonkish connectives.

Stephen Read (2000, forthcoming) has proposed a particular type of harmony, general-elimination harmony. Interestingly, under this constraint there is a tonkish connective who comes out as harmonious, and, perhaps surprisingly, Read accepts it. Let's give the rules for the connective, called bullet:

where the brackets indicate discharge of assumptions. (Feel free to ignore the double bullet in the elim-rule unless you have a problem with contraction. The strange form of the elim-rule is due to the generalization of the harmony function. Compare it to the general implication elimination, say. See Read (2000) for details on his harmony constraint.)

First, what's bad about bullet? In Read's words, bullet is pathological -- the fate of any "bulleted" (loaded?) system is inconsistency. In fact, on this account, bullet is even worse than tonk: it gives you inconsistency even without a negation (i.e., anything is provable). In comparison, tonk only gives you inconsistency if there is a negation around (without it it gives you that anything is provable from any non-empty set of premises). But, subtleties aside, the point is simply that bullet is equivalent to its negation. Thus Read's honorific: A proof-theoretic Liar.

What's good about bullet? It appears to be harmonious. Take the obvious normalization reduction step from conjoining bullet-intro and -elim, and it behaves as expected, i.e., you can reduce away the maximal formula and proceed via a normal proof. (As is well-known, tonk fails on this account.) Read's answer is to bite the bullet (no pun intended). Although some have insisted, it is not the job of harmony to prevent inconsistency. If you stipulate a connective with a clearly devious intro-rule, then harmony can do nothing to prevent your system from acting up. All it can do is to provide you with the corresponding elim-rule.

In fact, seeing that a loaded system will be inconsistent, this is also a counter-example against conservativeness as harmony. For, needless to say, bullet will allow you to prove things in the antecedent language fragment that you couldn't prove before (granted that the original logic was consistent). This follows immediately: Bullet allows you to prove anything!

Here are some sequent calculus rules for bullet, and a conversion pushing the cut application in a bullet-derivation with both the L- and R-rule:


Conversion:


By the R-rule, we get a pretty good idea why bullet is equivalent to its own negation. But also, note that both bullet-rules have the nullary connective both in the premises and in the conclusion. On Dummett's terminology, then, the rules are not sheer. There is an associated worry that the intro-rule (R-rule) cannot be meaning-conferring if it includes the very connective in question in its canonical proof. I'm not going to discuss this here. Suffice to note that proof-theoretically this results in it being impossible to get rid of bullet as you proceed upwards in the tree. Contrast this to the run of the mill connective, where the subformula property is a frequent trademark. Fortunately for bullet, however, it shares that fate with significantly more distinguished connectives. One is the G3i (sequent calculus for intuitionistic logic with absorbed structural rules) L-rule for implication.