FOM: relevance and choice of logic

[Torkel Franzen]

  Neil suggests:

  >I think if you formalize Torkel's argument ...  you would find that
  >the assumption that p1,..pn are all the primes *does*
  >play a role, contrary to Torkel's suggestion.

  Sure it plays a role: we conclude that it is false. But how is the
assumption used in the reasoning? You say

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

  The argument establishing that there is a prime different from each of
p1,..pn doesn't use the assumption that p1,..pn are all the primes there
are. Indeed it doesn't even use the assumption that p1,..pn are primes.
Thus, as a matter of logical hygiene, one should transform the proof into
the form

          for any k1,...kn there is a prime different from all of
          k1,..kn. Hence there are infinitely many primes.

  >If your proof really is at first order, say in PA, then you will have used
  >instance I1,...,Ik of the induction axiom scheme.

  This is true of formalizations. In my actual proof, there may be some
implicit inductions that I don't even bother to spell out. I may be
interested, however, in observing that my proof is elementary. Thus I
regard the proof as establishing PA |- A for my theorem A.

  A formalization of my proof will give me more information: in fact
I1,..Ik,P0 |- A, where P0 consists of the PA axioms minus induction,
and I1,...Ik are some instances of induction. This further information
need not represent any epistemic gain whatever compared to PA |- A. In
fact, enumerating I1,..Ik may well be merely confusing and utterly
uninteresting, and what minimal I1,..Ik can be extracted from my proof
is not a question that has any apparent mathematical interest. (Whereas
mathematicians often consider it of interest just what
mathematical assumptions about spaces, functions and so on are
actually used in a given proof.)

  To be sure, logicians may take an interest in noting that only
induction instances of a certain degree of logical complexity have
been used, but even a logician will normally fail to find any
epistemic gain in knowing that A is provable using a particular list
of Delta-0 induction axioms.