FOM: relevance and choice of logic

[Neil Tennant]

I couldn't tell from my email header who sent the following in
response to my posting about relevance in logical reasoning, but I'd
like to reply briefly. The person in question wrote as follows:

____________________________________________________________________

>From owner-fom at math.psu.edu Thu Nov 20 08:44:10 1997


>From a mathematical point of view, the intuitionistic restriction
on logic makes sense as an element in preserving a global property
of proofs, that of being "constructive". Is there any corresponding
global property of proofs (meaningful from a mathematical point of
view) that the restrictions [Neil Tennant proposes] help preserve?
... Here I wonder which intuitions of relevance [NT has] in mind. One
interpretation would be the ideas mathematicians have about what is
used in some essential way in a particular proof and what could be
eliminated without any great amount of work, but it doesn't appear
that this is what [he has] in mind.

____________________________________________________________________

This *is* actually what I had in mind, but perhaps the amount of
detail that I provided immediately upon raising the topic obscured the
motivation.

Just as mathematicians have (reasonably) clear intuitions about what
counts as a constructive piece of reasoning, so too do they have
(reasonably) clear intuitions about what counts as a piece of
*relevant* reasoning.  They can sense when an assumption has *really
been used*, just as they can sense when some symbol (say, r) in a
proof stands for a *truly arbitrary real number*. Just as they would
generalize from F(r) to `for all reals x, F(x)' only when they
recognize that r is truly arbitrary, so too would they conclude to ~P
on the basis of a proof of absurdity only when they recognize that P
has really been used as an assumption in the proof of absurdity.

Now standard logical systems have nice formal requirements on
occurrences of parameters like r that ensure that applications of
universal introduction will be valid. The requirement (a purely
syntactic one) is that the parameter r should not occur in any
assumption on which F(r) depends. This makes r `logically hygienic'
for universal introduction.

Note how *that* requirement already involves being able to tell what
assumptions the subordinate conclusion F(r) itself depends on!

What is *missing* in standard logic is formal provision for ensuring
that the assumptions in a formal proof on which its conclusion
'depends' are the asumptions on which it REALLY DEPENDS, in the
context of that proof. THIS is what I am proposing to capture with my
alternative system of natural deduction (and, correspondingly, sequent
calculus).

There is a further `global condition' which indeed can be stated, and
whose satisfaction entails that a relevant logic has to be exactly of
the kind that I am proposing. The condition is what I call the
"Non-Forfeiture of Epistemic Gain" (NFEG). I can explain it briefly:

Suppose you have a proof of a conclusion A from a set X of premises.
Suppose then that someone comes along and offers you a proof that in
fact # (absurdity) follows from X. Take his proof!--it represents
epistemic gain. Similarly, suppose what he had offered was instead a
proof of A from some *proper subset* of X. Again, take his proof!--for
it represents epistemic gain. Indeed, the most extreme form of the
latter kind of gain would be where the proper subset in question was
the empty set; for then you would have learned that A was a logical
truth, and that you didn't need any assumptions for its proof.

Generalizing: you make epistemic gain when you discover a proof of a
proper subsequent of a sequent you have already proved.

Now, consider searching for a proof of a final sequent Y:B. (Perhaps Y
is a set of mathematical axioms, and B a conjecture you are trying to
prove.) Suppose that you have got a proof fragment Pi worked out to
the point where all you need, in order to complete a proof for Y:B, is
a sub-proof of some sequent X:A occuring higher up in the sequent
proof of Y:B under construction. So you set about looking for a proof
Sigma of X:A.

	Sigma ... the sub-proof you're looking for
    ---- X:A
    \    /
     \Pi/... the overall proof under construction
      \/
      Y:B ... the overall result to be proved

Suppose, now, that you do even better than Sigma---you
find a *gainful* proof Sigma*, of some *proper subsequent* X*:A* of X:A.
So you would like to be able to `plug in' Sigma* at the point within
Pi where you had planned to place Sigma:

	 Sigma* ... the gainful sub-proof you've found
    ---- X*:A* ... the epistemically gainful sequent
    \    /
     \Pi* ... what you hope will be a well-formed result
      \/
      Y:B ... the overall result to be proved

Now hear this!: many a system of relevance logic makes it impossible
for the overall result Pi* to now be a `relevant' proof! BUT, if we
insist on the Non-Forfeiture of Epistemic Gain, we are saying that by
putting Sigma* into the originally projected proof Pi at that point,
we should be able to get an overall proof with the structure of Pi
itself, or perhaps even some (shorter) proof Pi* that is better than Pi, in
so far as Pi* proves a *proper* subsequent of Y:B. Moreover, Pi* should
be effectively determinable (indeed, in linear time) from the last
configuration just displayed.

This, to my mind, is a useful kind of global property for a relevance
logic to have. It can be shown that NFEG uniquely determines the
logical rules (both natural deduction and sequent calculus) in both
the classical and the intuitionistic case. [Details can be found in
ch.10 of my book `The Taming of The True', OUP, 1997.]