[FOM] power set in math

[Arnon Avron]

On Sun, Sep 09, 2007 at 07:52:11PM -0400, Harvey Friedman wrote:
> On 9/9/07 2:49 AM, "Arnon Avron" <aa at tau.ac.il> wrote:
> 
> >  Thus in predicative mathematics the existence of {{n}: n\in N}
> > or of {[1/n,1-1/n]: n\in N} can be justified *only* by replacement -
> > exactly what the notations used by mathematicians reflect. This
> > is another demonstration of Weaver's thesis (put forward
> > in several postings to FOM and in his papers) concerning the
> > remarkable match that exists between predicatively acceptable mathematics
> > and normal mathematical practice.
> 
> In the proof of FLT (Fermat's last theorem), there is substantial use of
> power set applied to infinite sets. As pointed out by McLarty on the FOM,
> there is not even a documented proof of FLT without using a strongly
> inaccessible cardinal, as the documented proof passes through the rather
> abstract work of Grothendieck that relies on strongly inaccessible
> cardinals. 

First, I should clarify that this fact does not refute what I have
written in the quotation above. "remarkable match" does not mean
identity, and I have never claimed (nor is it true)
that mathematical practice *always* follows predicativist principles,
or that mathematicians never use the powerset axiom. Thus rigorous 
books on analysis start by introducing the real numbers (usually
as Dedckind cuts), and it would be foolish to deny that in this case
not only the official argument, but also the intuition behind it,
are based on the powerset axiom. In such cases it is our (the
predicativists) task to try to explain/justify as far as possible
these clear violations of predicativist principles. The ultimate goal 
in such cases is to "allow" mathematicians to continue to do things
the way they usually do, but to show that the final result
is nevertheless predicatively justified. This is not always
possible, of course, and so at least I (I do not want and I cannot
speak in the name of all predicativists) distinguish between
different degrees of certainty that mathematical proofs provide.
Thus if the alleged proof of FLT indeed requires the use
of inaccessible cardinals, then FLT has *not* been proved yet
with absolute mathematical certainty. The "proof" in this case
would only give the truth of FLT a very high degree of plausibility,
and perhaps (I am not claiming this!) would give us greater confidence 
in the truth of FLT than in our confidence that the sun will shine 
tomorrow or that none of us will live forever (because even I do not
really doubt that the required axioms of strong infinity are
consistent - and this consistency is all that one needs in this
case).  However,  providing confidence, no matter how strong, is not the
same as providing an absolute mathematical proof.
 
> Moreover, it would appear that any proof of FLT in anything even close to PA
> would be significantly more involved than the existing proof.

This is exactly what should be expected. The whole point of using "ideal"
methods is that they allow shorter and less complicated proofs
(isn't this what Hilbert's program was about?). 

One more crucial point: I know that again I'll find myself in a small
minority, but for me a mathematical theorem can be said to be
fully proved only when the alleged proof reaches the stage in
which it is presented in a readable textbook, in a way that
"the mathematician in the steet" (like myself) who so wishes
can follow and check for himself/herself (and see for sure what
are the underlying assumptions, e.g., whether assumimg the consistency
of a large cardinal axiom is essential for the proof or not!). It is 
evident from the discussion concerning its underlying assumptions 
that the alleged proof of FLT has not reached this stage yet.

SHANA TOVA!

Arnon Avron