[FOM] What produces certainty in mathematical proofs?

[Harvey Friedman]

On 9/14/07 1:02 AM, "Martin Davis" <martin at eipye.com> wrote:

>I had a colleague who refuses to accept
> any non-constructive proof I don't have an
> example at hand, but I suspect that there are
> non-constructive proofs that are fully
> predicative as that notion is usually explicated.

A very interesting example is that of Thue-Seigel-Roth theorem in number
theory http://en.wikipedia.org/wiki/Thue-Siegel-Roth_theorem which is of
logical form Pi03. We don't know if there is a constructive proof, but the
original proof is certainly predicative, as it is carried out in weak
fragments of PA. In fact, if my memory serves me right at all, in EFA =
exponential function arithmetic = ISigma0(exp). By the way, in what sense
can it be proved in even weaker systems?

Here is an example that is easily predicatively provable, but is *known* to
have no constructive proof:

Every bounded infinite sequence of rationals has a convergent subsequence.

> Going in the other direction, here in Berkeley
> there are logicians who accept very large
> cardinals without a qualm, whereas another
> equally fine logician has devoted a great effort
> in attempting to prove the inconsistency of the
> existence of measurable cardinals with ZFC.

Even the Berkeley people who accept very large cardinals without a qualm,
have their limits. They apparently have qualms about the very strongest ones
not subject to Kunen's inconsistency proof. I.e.,

"there exists a nontrivial elementary embedding from some V(kappa + 1) into
(kappa + 1)".

or even 

"there exists a nontrivial elementary embedding from some V(kappa) into
(kappa)".

I think it is the John Steel view that until there is a sensible "inner
model theory" for a large cardinal, then he has qualms, and people should
have qualms. 

> Harvey Friedman has emphasized the progression of
> means of proof from the most basic to the highest
> regions of the transfinite with a decision to
> draw the line at at particular level a matter of
> personal idiosyncrasy rather than the result of philosophical acumen.

In recent years, I like to push this all the way down into the "ultrafinite"
where one is talking about, say, functions and relations on {1,2,...,100} or
{1,2,...,1000}.

Nevertheless, there is still a lot of room for deep philosophical work.
Specifically, to catalog. and clarify the scope of, various foundational
positions. E.g., through striking completeness and incompleteness theorems.
> 
> There are two further points I'd like to make.
> One is that, in the last analysis mathematics is
> a social activity,  and as time goes on, methods
> that achieve desired results without leading to
> catastrophe will just gain acceptance.

This is probably going to continue to be the case. Unless  catastrophes
emerge from time to time. Then people will shift, emphasizing that one
cannot be complacent. HOWEVER, this has not happened. The closest to it is a
very weak case of the Kunen inconsistency in 1968 or so, with, in modern
form,

"there exists a nontrivial elementary embedding from some V(kapa + 2) into
V(kappa + 2)". 

Incidentally, the refutation uses AxC, and nobody has refuted this in ZF.

> Harvey's work gives tantalizing examples, but so
> far there is no example of a true Pi-0-1 sentence
> that number theorists have longed to prove but
> which requires set theoretic, or even highly
> transfinite, methods for its proof. Gödel himself
> once suggested that the Riemann Hypothesis could be such a proposition.
> 
Direct attack on this problem seems hopeless.

The plan is to develop a series of examples that are increasingly
fundamental, simple, tantalizing, attractive, etc. It remains to be seen how
far this process will go. I conjecture that it will ultimately impact every
field of mathematics in a serious and practical way. When the dust settles,
maybe I will be remembered.

Harvey Friedman