FOM: relevance and choice of logic

[Neil Tennant]

Torkel raises some interesting points, but I don't think they contradict what I said about relevant proofs. I think if you formalize Torkel's argument

          suppose p1,...pn are all the primes. Then either
          (p1*..*pn)+1 is itself a prime, or [it] 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

you would find that the assumption that p1,..pn are all the primes *does*
play a role, contrary to Torkel's suggestion. I interpret the conclusion 
in the context of this argument as stating

	For no natural number n is it that case that the first n
	primes are all the primes there are.

To prove this, suppose for reductio that n is a natural number such that
the first n primes are all the primes there are. Let these primes be
p1,...,pn. Consider now the number (p1*..*pn)+1. Clearly it is distinct 
from each pi. Moreover, ...

	[Now pick up Torkel's argument from here:]

							... either
          (p1*..*pn)+1 is itself a prime, or [it] is divisible by
          a prime different from each of p1,..pn. 

In each case it would follow that there was a prime distinct from each
of p1,...,pn. But this is contrary to our assumption about n and p1,...,pn.
Thus it is not the case that for some natural number n, the first n primes 
p1,..pn are all the primes there are. That is, there are infinitely many primes.

So, Torkel, I think this example fails to be an example of a stated assumption 
turning out to be logically irrelevant.

That is not to say that there aren't other way of establishing the same 
conclusion, especially if one formalizes it differently--say, as the claim

	for every natural number k there is some prime greater than k.

Here, one would proceed as follows. Let m be an arbitrary natural number.
There are at most finitely many primes less than m. Suppose there are n
of them. Let p1,...,pn be the primes less than or equal to m. 
Consider now the number (p1*..*pn)+1. Clearly it is distinct from each pi. 
Moreover, by excluded middle (acceptable to an intuitionist, since the
sentence in question is effectively decidable), either 
	(1) (p1*...*pn)+1 is itself a prime, or 
	(2) (p1*...*pn)+1 is not itself a prime
Case (1): Suppose (p1*..*pn)+1 is itself a prime. 
   Sub-case (A): Suppose (p1*...*pn)+1 is less than or equal to m. 
   Then we have a contradiction, since p1,...,pn themselves were supposed 
   to be all the primes less than or equal to m. 
   Sub-case (B): Now suppose (p1*...*pn)+1 is greater than m. Then we have
   the result we seek.
Case (2): Suppose (p1*...*pn)+1 is not itself a prime. Then it is divisible 
by some prime. Let such a prime be q. It follows that q is different from 
each of p1,..,pn, since these do not divide into (p1*...*pn)+1 without 
remainder.
   Sub-case (A): Suppose q is less than or equal to m. Then we have a 
   contradiction, since p1,...,pn themselves were supposed 
   to be all the primes less than or equal to m.
   Sub-case (B): Now suppose q is greater than m. Then we have
   the result we seek.
It follows (by multiple proof by cases) that there is some prime greater than m.
But m was an arbitrary natural number.
Therefore for every natural number k there is some prime greater than k.

Note how nicely the salient parts of this proof fit the pattern I gave for
v-Elimination (proof by cases). We close off one case with absurdity, and
then simply proceed to the conclusion of the other case.

The informal proof has had to be presented at this length in order to make it
clear exactly how it would be formalizable as a natural deduction.

Torkel's other main point was:
_________________________________________________________________
 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.
___________________________________________________________________

If your proof really is at first order, say in PA, then you will have used
instance I1,...,Ik of the induction axiom scheme. Your conclusion A would 
be proved from I1,...,Ik plus whatever other axioms X you might have used.
Suppose, then, that your proof Pi is as follows:

	X, I1,...,Ik
	\	    /
	 \   Pi    /
	  \       /
	   \     /
	    \   /
	      A

Now, if I can show you a way to transform this proof Pi into a proof Pi*
that does not appeal to, say, Ik:

	X, I1,...,Ik-1
	\	    /
	 \   Pi*   /
	  \       /
	   \     /
	    \   /
	      A

surely this would be better? Moreover, it would show that your proof Pi
did not really use the instance Ik of induction. (Note that I am not
suggesting that I find a totally different proof Pi*, using a different
`line of reasoning'; rather, I am suggesting that your very proof Pi might
`boil down' to this simpler proof Pi* once you attend closely to questions
of relevance, and genuine use of assumptions.)

The assumption Ik that is no longer needed might lie in a completely different
complexity class from I1,...,Ik-1; so there could be real interest in having
made the proof free of any appeal to Ik.

And if you don't like that point, perhaps because you believe that all instances
of induction are on an epistemic par, I could still point to the possibility
that it is one of the other `non-inductive' assumptions in the set X, say, that could turn out to be irrelevant *for the line of reasoning that you are trying 
to present by means of Pi. *

(Note that that last star is not a superscript to Pi, but a punctuation mark
for email emphasis!)

Neil Tennant