[FOM] Relevance Logic and Tennant

[Neil Tennant]

I'm grateful to Harvey Friedman for responding in
http://www.cs.nyu.edu/pipermail/fom/2013-August/017535.html
to my posting about Core Logic in 
http://www.cs.nyu.edu/pipermail/fom/2013-August/017528.html ) 
and then for writing again in
http://www.cs.nyu.edu/pipermail/fom/2013-August/017544.html
to help avert some of the mistaken impressions that his first response might have raised.

I would like first to clear up the matter of misuse (or lack of it) of standard terminology. 
If readers re-visit my posting about Core Logic, they will find that it scrupulously avoids any allegations of invalidity on the part of any forms of inference that the intuitionist logician regards as valid (or, for that matter, any forms of inference that the classical logician regards as valid). The concern was solely with how best to capture those inferences whose premises bear a relation of relevance to their conclusions (however that relation of relevance might be explicated). I should perhaps have warned my reader that I was using 'relevance' in an intuitive, informal sense, in which there was no commitment to the sorts of views espoused by relevance logicians in the Anderson-Belnap tradition. So perhaps I should have used a subscripted term, like 'relevance_ii', to indicate that. (Here, 'ii' is short for 'intuitive, informal'.) Please take my original posting as hereby uniformly amended in that regard.

This would also be an appropriate occasion to bring to the reader's attention how, in fact, the eventual explication of relevance embodied in Core Logic differs from that of relevance logicians in the Anderson-Belnap tradition. The best contrast can be found in the possible responses to Lewis's now famous little proof of 'A, not-A, therefore B'.  If you can prove the sequent

    A => AvB

and can prove Disjunctive Syllogism:

    AvB, not-A => B

then by one application of Cut you can prove

    A, not-A => B.

All relevantists wish to avoid proving this last result. Some relevantists go so far as to say that it is invalid. I do not. To be sure, it is valid in both the intuitionistic and the classical senses. But its premises lack that relation of relevance that we wish to see between premises and conclusions of arguments that we (relevantists, in the ii-sense) are to be able to prove.

Apart from the odd outlier in the tradition, virtually every relevantist has no problem with v-Introduction ('A => AvB'). So, to avoid commitment by proof to Lewis's paradox ('A, not-A => B'), there are only two possible choices:

1. Make it impossible, in your system of relevance logic, to prove Disjunctive Syllogism ('AvB, not-A => B'); or
2. Do not allow proof-formation by steps of (unrestricted) Cut.

The Anderson-Belnap tradition opted for (1), and hung on to unrestricted Cut as a rule in their system R.

I opted for (2), and hung on to Disjunctive Syllogism, for the system of Core Logic.

         A-B    NT
DJ     no      yes
Cut    yes    no

Another point of contrast between the Anderson-Belnap tradition and Core Logic is that A-B focuses on the object-language conditional arrow, whereas the Core Logician focuses on the turnstile of deducibility.

For the system of Core Logic (and for its classicized extension), which lacks any proof-forming rule of Cut, we nevertheless have the very important result that Cut is admissible. It is so in the sense given by the following metatheorem, which was stated in my original posting:

     There is an effective operation * such that: 
     given any Core proof P1 of the sequent X => A, and Core proof P2 of the sequent A,Y => B, 
     P1*P2 is a Core proof of (some subsequent of) X,Y => B.

What, now, is the dialectic between the Core Logician and the Classical Logician? Since they have the same initials, let us call these two characters NT and HF, respectively.

HF: You say you're a relevance logician. I've looked up you guys in Wikipedia, in the Stanford Encyclopedia of Philosophy, on Greg Restall's blog, and in a paper by John MacFarlane---and apparently you're all busy rejecting as invalid various standard classical moves that are clearly valid. What's going on?? How can you possibly hope to give a logical foundation for mathematics?

NT: I'm a relevance logician who hopes to guide you to the discovery of the essential core of worthwhile inferential moves, deep inside Classical Logic, which actually happen to suffice for all mathematical reasoning. 

HF: What do you mean by 'all mathematical reasoning'? 

NT: By 'all mathematical reasoning' I mean all possible deductions of mathematical theorems, in a first-order language, from the mathematical axioms of whatever theory the mathematician is working in. As logicians, we are trying to provide deductive systems that can naturally formalize, or regiment, passages of reasoning by mathematicians that are informal, even when published in journals and textbooks. No mathematician actually writes down a formal natural deduction, or formal sequent proof! 

HF: But I use Cut all the time! I do so every time I prove a Lemma, and then appeal to that Lemma subsequently when deriving a theorem! And apparently you reject Cut!

NT: No, I do not reject Cut. I just don't need it as a rule that is applied within the system. Gentzen, after all, showed in his Hauptsatz that every proof containing an application of Cut could be transformed into one that contains none. 

HF: Yes, but Gentzen resorted to lots of Thinnings in his proof of Cut-Elimination! And you reject also (sorry: eschew also) the structural rule of Thinning (on the left or on the right). You're trying to have your cake and eat it.

NT: Poor Gentzen only resorted to Thinnings because he needed them in order to obtain a Cut-free proof of the original target sequent. What Gentzen failed to notice was that he could have gone on to establish another Hauptsatz (let us call it Thinning-Elimination), to the effect that any Cut-free proof of a given sequent can be turned into a Cut-free, Thinning-free proof of some subsequent of the given sequent. And that's the insight behind the cut-admissibility result for Core Logic: any 'overall sequent' that you think you should be able to obtain, courtesy of Cut, actually contains a subsequent that is Core-provable. 

HF: But then you're cheating! You're not giving me a proof of the overall result that I get when I apply Cut in my system.

NT: Your last remark is quite right. But I'm not cheating at all. For the system of Core Logic gives you something even better: it gives you a possibly logically stronger result than the one you thought you would be getting.

HF: How so?

NT: Well, suppose you thought you would be getting the sequent X => A, by applying Cuts (and perhaps also Thinnings). In Core Logic, you would get (for some subset X' of X) either a proof of X' => A, or a proof of X' => emptyset. So EITHER you would be getting a Core proof of your desired mathematical theorem A from (possibly fewer) axioms X' than you had used before; OR you would be discovering the inconsistency of your chosen axioms.

HF: But that last thing would never happen. Mathematics is consistent. Or at least, any set of axioms that I decide to employ is definitely consistent.

NT: Then you have absolutely nothing to worry (or complain) about. Because now, applying Disjunctive Syllogism in the metalanguage, I can assure you that the Core proof you get will be of the former kind: a proof of your theorem A from some subset X' of your original (consistent!) set X of axioms.

HF: But how come you can do this? What about my applications of Cut?

NT: Those 'applications' of Cut need not ever be regimented as steps of inference taken within a formal proof. The only proofs in mathematics that need to be regimented are the ones 'in between' your Lemmas. (Lemmas, for the logician, are just interpolants.) The regimenter need only focus on those passages of proof that appear in well-written mathematics articles and books after the heading 'Proof:', and before the 'QED' at the end. I've noticed, in fact, that your own deductive practice is a very good example of this. You never, as it were, prove a Lemma within a proof of another one. Rather, you state all your Lemmas in a sequence, and appeal in your proofs of them only to Axioms, and to previously stated-and-proved Lemmas and Theorems and Corollaries. Your actual nitty-gritty passages of reasoning, where all the careful deductive work is done, are Cut-free!

HF: I had never though of that! I feel like Monsieur Jourdain, who was overjoyed to discover that he had been speaking prose all along! So you're saying I've just been doing my thing in (classicized) Core Logic all along?

NT: Yes, indeed, I do. And may I flatter you further, by pointing out that, while the real deductive work is in the Cut-free details, nevertheless the truly inspired aspect of an overall proof is the series of choices you make of Lemmas on the way. For they are the interpolants, with respect to which 'cuts' take place. By interpolating them, you achieve at times hyperlogarithmic reduction in overall length of proof. Keep doing this, HF! Progress in mathematics depends on it. But, for the purposes of a logician who simply wishes to provide regimentations of mathematical deduction, the real work lies in being able to formalize those cut-free bits of reasoning. You do need, mind you, a metatheorem in the background, guaranteeing the admissibility of Cut. Moreover, given that it takes that lovely form in which you potentially discover (a proof of) a stronger result than the one you thought you had proved, it has much to commend it.

HF: I just love this! So where Gentzen said 'Here, HF, you have proved this Lemma, and then have used it to prove your theorem! Now apply Cut to get your overall proof!', you simply say 'Nice proof of, and subsequent use of, that Lemma, HF! Now rest assured that there is an effectively determinable proof of a result at least as strong as the result you wish to have proved, and possibly even stronger!' OMG, this is the kindest cut of all!

NT: I want to extract for you the kernel of logic, HF, without the surrounding dross. I want to show you that you can eschew the dross. You have no methodological need for it. Everything you prove can be proved without it. You've been doing it all along. I'm so glad that making you aware of an essential feature of your own past practice can cause you such foundational joy!

Exeunt ad tavernam.