[FOM] Relevance Logic and Tennant

[Arnon Avron]

Neil,

I do not want to start a long debate (which is why I have hesitated
to reply to your message). Still, I would like to make
a few comments in order to show 
that things are more complicated than what your message implies.
 
> Apart from the odd outlier in the tradition, virtually every relevantist 
> has no problem with v-Introduction ('A => AvB'). 

I believe that this is somewhat misleading. In relevance logics
at least two "disjunctions" are considered:  the intensional (or
"multiplicative" in the terminology of Girard) and the extensional
(or "additive"). Each of them has the same right to be taken 
as the counterpart of classical disjunction. Now the extensional 
disjunction indeed satisfies v-Introduction but not the
Disjunctive Syllogism, but it is the other way around 
with the intensional disjunction.  
  Let me add here that relevance logics can actually do very 
well without the "extensional connectives" (which in my opinion
only cause troubles, and totally destroy the motivations
given by the relevantists for the implicational fragments of their logics).
In contrast, they have practically no value without 
their intensional implication and negation (and so also
their intensional disjunction and conjunction).

>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.

Please look e.g. at my paper (available from my homepage):

"Combining Classical Logic, Paraconsistency and Relevance"
(Journal of Applied Logic 3, 133-160, 2005)

And you'll find out that there is a third possibility,
better in several ways than the two you mention above.


 
> 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. 

Gentzen's theorem does not apply to reasoning in general.
Thus the cut rule is indispensable for the natural Gentzen-type
system(s) for ancestral logic (which of course are not complete,
but very valuable nevertheless). So this argument from Gentzen's
theorem has no force unless you insist that logic
is first-order logic, and there is nothing beyond (a view
I strongly oppose).

Actually, your argument is problematic even  on the
first-order level. Thus already for first-order logic
with equality one should allow the use of "inessential cuts"
(Gentzen's terminology) in a reasonable proof system. Moreover:
cut can in principle be dispensed with only for what I
called many years ago  the "truth" consequence relation
of classical logic, not the "validity" consequence relation,
according to which, e.g.  \forall x A follows from A.
(The validity CR is for example the one that Shoenfield
is using throughout his classical book. This is why he talks
about "open theories" where other talk about "universal theories").
Now from the point of view of Gentzen-type systems, a formula B
truth-follows  from  a set T of formulas  iff there is
finite \Gamma such that the sequent \Gamma=>B is derivable in LK,
while B validity-follows  from T iff there is
finite \Gamma such that the sequent =>B follows in LK
*using cuts* from {=>A: A in \Gamma} (if I remember correctly, this is
the official definition of the first-order consequence
relation in Takeuti's "proof Theory"). Note that the use of cuts
is essential in the case of the validity CR!

Arnon Avron