FOM: Relevance and mathematical modeling: a case in point

[Jon Barwise]

Neil raises the question of relevance in mathematical reasoning.  I think
this is an interesting issue.  Why is it that mathematicians who do not
know of a principled response to, say, Russell's paradox, not worry about
it, as long as it is not relevant to their branch of mathematics?  They
would never try to publish a proof of the Reimann Hypothesis (RH) by
assuming it was false, using Russell to get a contradiction, and then
claiming RH.

To my way of thinking, though, standard relevance logic attempts to get at
this question are unsatisfying.  They seem to be an example of what a
mismatch model and reality can lead to, in this case, between mathematical
proofs and the relevance logician's mathematical models of proofs.

In mathematics, when attempting to prove some claim B, one often needs to
break into an exhaustive range of cases C1,...,Cn.  Some cases are
typically eliminated as leading to absurd conclusions.  If in the remaining
cases one establishes B, then B follows clearly.  This is an absolutely
crucial form of reasoning.

How do we model this in our formal models of proof, say natural deduction
models?  Well, the ones I am familiar with opt for elegance.  The method of
proof by cases is modeled by v-elimination.  Prove C1 v ... v Cn.  Break
into cases C1, ... Cn, and establish B in EACH of them.

As long as we model proof by cases in this way, then we need the move from
the absurd to B to allow us to model the above form of reasoning.  A less
elegant way to do it, but one that would more faithfully model the actual
reasoning, would be to formulate proof by cases in a way that would allow
one to establish either B or the absurd in each case, and then conclude B.
I am not sure what the upshot of this direction would be.  (Probably there
are formal systems that take this approach.)

I confess to not having understood Neil's message well enough to know that
my criticism applies, but in general, taking an existing logic and throwing
out rules, like the rule of the absurd to B, can become a very artificial
exercise, one divorced from the proof practices one is interested in
modeling.  In particular, it does seem to me to get at the real issue of
relevance in mathematical reasoning.

Jon