[FOM] power set in math

[Harvey Friedman]

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. 

As pointed out by Solovay on the FOM, it is reasonably clear that the proof
of FLT can be reasonably conveniently done in something like third order
arithmetic - thus using P(N) seriously, and perhaps PP(N) weakly. Of course,
Bob usually speaks for himself.

It is my own personal conjecture that not only can FLT be proved in PA
(Peano arithmetic), but also in EFA = exponential function arithmetic.
However, even a proof in PA is apparently rather far from being documented.

Moreover, it would appear that any proof of FLT in anything even close to PA
would be significantly more involved than the existing proof.

In any case, mathematicians have apparently gravitated in their expositions
of the FLT proof and the related algebraic and number theory material, to
outright using power set applied to infinite sets.

About the future: I have no doubt that Boolean Relation Theory will be fully
accepted as normal discrete mathematics in the relatively near future. The
book on BRT should be available on the web quite soon. Here more than ZFC is
used in order to prove statements in discrete mathematics that are even
effectively true. This use *cannot* be avoided.

Harvey Friedman