FOM: relevance and choice of logic

[Torkel Franzen]

  Neil Tennant says:

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

 Let's see if I understand you correctly. In mathematics, we say
e.g. such things as "differentiability of f is assumed in the proof, but
this is clearly inessential", when we see how the proof could easily
be recast so as to avoid this assumption. In such a case, though, the
inessential assumption will in general be logically relevant in the
proof as it stands. What you have in mind are *logically* irrelevant
occurrences of assumptions in mathematical proofs.

  No doubt mathematicians have on the whole a good appreciation of
when assumptions are logically irrelevant. (This does not hold without
exception, though - I have seen several mathematicians put forward
the argument

          suppose p1,...pn are all the primes. Then either
          (p1*..*pn)+1 is itself a prime, or is divisible by
          a prime different from each of p1,..pn. Thus
          it is not the case that p1,..pn are all the primes,
          so there are infinitely many primes

without any apparent sensitivity to the circumstance that the
assumption that p1,..pn are all the primes doesn't really have any
role to play in the argument.) However, this property of proofs
doesn't seem to be all that important. Mathematicians traditionally
devote a lot of work to showing assumptions to be mathematically
unnecessary (and to showing that proofs or results can be made
constructive), but given the formulation of a result - "every fnorgle
is a blurgle" - it doesn't seem to matter greatly whether the proof of
this result uses, internally, logically irrelevant assumptions.

  It's not obvious that mathematical proofs in general should be
free of logically irrelevant assumptions even as a matter of
logical hygiene. You suggest that

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

  The problem with this is that since you're talking about logical
derivations in first order logic, my mathematical proof will be represented
as a derivation from, say, the axioms of PA or Z. Here I'm usually
not interested in knowing just which instances of the induction
axioms or comprehension axioms I have used in my proof, and won't
think that it represents any epistemic gain to know that my proof
can be formulated so as to use some specific instances of those axioms.

  >I couldn't tell from my email header who sent the following in
  >response to my posting about relevance in logical reasoning, 

  Sorry about that; I'll include a signature.

  Torkel Franzen