The revised, surely-more-natural, disjunction elimination rule mentioned in the last post is, of course, Neil Tennant’s long-standing proposal — and the quote about the undesirability of using explosion in justifying an inference like disjunctive syllogism is from him. This revision has, I think, considerable attractions. Even setting aside issues of principle, it should appeal just on pragmatic grounds to a conservative-minded logician looking for a neat, well-motivated, easy-to-use, set of natural deduction rules to sell to beginners.

But, in Tennant’s hands, of course, the revision serves a very important theoretical purpose too. For suppose we want to base our natural deduction system on paired introduction/elimination rules in the usual way, but also want to avoid explosion. Then the revised disjunction rule is just what we need if we are e.g. to recover disjunctive syllogism from disjunction elimination. And Tennant does indeed want to reject explosion.

Suppose, just suppose, that even after our logic teachers have tried to persuade us of the acceptability of explosion as a logical principle, we continue to balk at this — while remaining content e.g. with the usual remaining negation and conjunction rules. This puts us in the unhappy-looking position of accepting the seemingly quite harmless \(P, \neg(P \land \neg Q) \vdash Q\) and \(\neg P \vdash \neg(P \land \neg Q)\) while wanting to reject \(P, \neg P \vdash Q\). So we’ll have to reject the unrestricted transitivity of deduction. Yet as Timothy Smiley put it over 50 years ago, “the whole point of logic as an instrument, and the way in which it brings us new knowledge, lies in the contrast between the transitivity of ‘entails’ and the non-transitivity of ‘obviously entails’, and all this is lost if transitivity cannot be relied on”. Or at least, all *seems* to be lost. So, at first sight, restricting transitivity is a hopeless ploy. Once we’ve accepted those harmless entailments, we just have to buy explosion.

But maybe, after all, there is wriggle room (in an interesting space explored by Tennant). For note that when we paste together the proofs for the harmless entailments we get a proof which starts with an *explicit* contradictory pair \(P, \neg P\). What if we insist on some version of the idea that (at least by default) proofs *ought* to backtrack once an explicit contradiction is exposed, and then one of the premisses that gets us into trouble needs to be rejected? In other words, in general we cannot blithely argue past contradictions and carry on regardless. Then our two harmless proofs cannot be pasted together to get explosion.

But how can we restrict transitivity like this without hobbling our logic in the way that Smiley worried about? Well suppose, just suppose, we can arrange things so that if we have a well-constructed proof for \(\Gamma \vdash \alpha\) and also a well-constructed proof for \(\Delta, \alpha \vdash \beta\), then there is EITHER a proof of \(\Gamma, \Delta \vdash \beta\) (as transitivity would demand) OR ELSE proof of \(\Gamma, \Delta \vdash \bot\). Then perhaps we can indeed learn to live with this.

Now, Neil Tennant has been arguing for decades, gradually revising and deepening his treatment, that we *can* arrange things so that we get that restricted form a transitivity. In other words, we can get an explosion-free system in which we can paste proofs when we ought to be able to, or else combine the proofs to expose that we now have contradictory premisses (indeed that looks like an epistemic gain, forcing us to highlight a contradiction when one is exposed). On the basis of his technical results, Tennant has been arguing that we *can* and *should* learn to live without explosion and with restricted transitivity (whether we are basically classical or intuitionist in our understanding of the connectives). And he has at long last brought everything together from many scattered papers in his new book *Core Logic* (just out with OUP). This really is most welcome.

Plodding on with my own book, I sadly don’t have the time to comment further on this Tennant’s book for now. But just one (obvious!) thought for now. We don’t have to buy his view about the *status* of core logic (in its classical and constructivist flavours) as getting it fundamentally *right* about validity (in the two flavours). We can still find much of interest in the book even if we think of enquiry here more as a matter of exploring the costs and benefits as we trade off various desiderata against each other, with no question of there being a right way to weight the constraints. We can still want to know how far can we go in preserving familiar classical and constructivist logical ideas (including disjunctive syllogism!) while avoiding the grossest of “fallacies of irrelevance”, namely explosion. Tennant arguably tells us what the costs and benefits are if we follow up one initially attractive way of proceeding — and this is a major achievement. We need to know what the bill really is before we can decide whether or not the price is too high.

Rowsety MoidI think I might be missing something that ought to be obvious here, but anyway: how do we avoid getting ‘explosion’ just from truth tables (or from truth tables plus the deduction theorem)?

(BTW, I find the Gentzen way of writing natural deductions quite opaque and unnatural.)