FOM: grand conjectures

[Harvey Friedman]

In a way, this is a response to Martin Davis 4/15/99 16:48:

>WHAT ELSE IS THERE TO TALK ABOUT?

In a separate posting, I will respond to McLarty because McLarty has
indirectly responded to Davis' question by recirculating a favorite analogy
of his between Friedman and Grothendieck that I already refuted earlier on
the FOM, and which exposes his hidden agenda which goes far beyond what
Davis lists as the series of events.

But now for something really productive.

Conjuecture 1. Every theorem published in the Annals of Mathematics whose
statement involves only finitary mathematical objects (i.e., what logicians
call an arithmetical statement) can be proved in EFA. EFA is the weak
fragment of Peano Arithmetic based on the usual quantifier free axioms for
0,1,+,x,exp, together with the scheme of induction for all formulas in the
language all os whose quantifiers are bounded. This has not even been
carefully established for Peano Arithmetic. It is widely believed to be
true for Peano Arithmetic, and I think that in every case where a logician
has taken the time to learn the proofs, that logician also sees how to
prove the theorem in Peano Arithmetic. However, there are some proofs which
are very difficult to understand for all but a few people that have
appeared in the Annals of Mathematics - e.g., Wiles' proof of FLT.

I now want to make a distinction between two kinds of elimination of uses,
with some examples.

A. There is elimination of uses by restriction.  One may typically do
something like this:

"Let F be a finite field. Let F* be its algebraic closure. See Lang's
Algebra for background to this paper."

One looks up Lang and sees

"Every field has a unique algebraic closure (up to isomorphism)."

Now this fake use of every field has an algebraic closure can be eliminated
by replacing the above with:

"Every finite field has a unique algebraic closure (up to isomorphism)."

But an even better replacement - a replacement that might well be needed - is:

"Every finite field has a unique algebraic closure (up to isomorphism)
which is countable."

This kind of elimination by restriction indicates that the use is fake.

B. More profound elimination of uses.  Here is an example. Various
important mathematicians worked very hard in showing that various ideals in
polynomial rings over standard rings and fields are finitely generated
(elimination theory people). Then Hilbert cam along and proved that every
ideal in these settings is finitely generated - and by an argument that,
although more abstract, was much simpler (Hilbert's basis theorem). It is
now known through work of Simpson (Ordinal numbers and the Hilbert basis
theorem, JSL, 1988?) that this theorem is proof theoretically significant
in the sense of reverse mathematics; he calculated that it is provably
equivalent to "omega^omega is well ordered" over RCA_0.

The earlier work (elimination theory people) showed that you can eliminate
the use of Hilbert's basis theorem in virtually all concrete contexts. But
this is not elimination by restriction!!! It is much more profound than
that. These are seriously different proofs!!! Furthermore, the earlier
proofs give more concrete information - number and degrees ideal basis
elements, etcetera. This kind of information is known to be unobtainable
from the Hilbert basis theorem alone.

C. Reflect on the difference: elimination by restriction, and elimination
by new proofs.

Now we come to the second conjecture.

Conjecture 2. All traces of logcially strong categorical methods (i.e.,
universes, topoi, etcetera), either explicit or referred to in any way,
shape, or form in the references, in the proofs of Theorems in the Annals
of Mathematics, can be eliminated by restriction in the sense of A above.
In other words, they are all fake uses in my sense. I.e., when fully
eliminated, the proofs are not new.

For instance, I indicated how I expect that the Riemann surface patching
case McLary presented in his 2:03PM 4/14/99 could be eliminated by
restriction. I wrote:

>Reply to McLarty 2:03PM 4/14/99. This posting of McLarty contains a
>disucssion of some set theoretic constructions which are far far weaker
>than universes. But even here, they appear to be fake uses. Since the
>relevant Riemann surfaces are separable, when approximating a global
>function one needs to look at only unions of countably many approximates
>defined on open sets. Presumably it is trivial to get rid of the hot air
>and do countable constructions - i.e., pasting at most countably many
>functions together. Perhaps the best way to get rid of the hot air also by
>considering only a countable basis for the open sets - i.e., a countable
>collection of open subsets of S such that every open subset of S is a union
>of these open subsets of S - rather than all of the open sets.

Martin Davis: is this a better posting?