[FOM] Certainty in mathematical proofs

[Harvey Friedman]

On 10/19/07 6:45 AM, "Arnon Avron" <aa at tau.ac.il> wrote:

> If pushed with determination, than there will
> be no escape from the claim that certainty is
> at the end a personal matter, and that one
> can never be certain about what is certain.
> If we leave the issue at that, then there is no
> point in discussing FOM. The only choice would
> be: everyone for himself/herself, and that's it.

FOM has traditionally been used on this list to refer to the list itself.
And f.o.m. has been traditionally used for "foundations of mathematics". I
assume that by FOM you mean f.o.m.

There are many reasons to study f.o.m., even if "certainty is a personal
matter". For example, certainty may be a personal matter now, because we
don't know enough - but NOT a personal matter later, when we do know enough.
And how can be get to know enough so that certainty is no longer a personal
matter? - by developing and studying f.o.m.
> 
> Well I, for one, do think that it makes sense to
> discuss and make research on FOM - and *for the
> original goal*: to provide  secure and certain
> foundations for large parts of mathematics,
> and to do so on the basis of *objective* criteria,
> which goes beyond someone's personal feelings and judgements.

At the present time, along the classical foundational lines, what looks
hopeful at the moment is to consider issues of relative security, and
careful formulations, and to classify actual mathematical arguments in terms
of relative security.

There are many other issues that arise when working on classical f.o.m.,
such as lengths of proofs, and structure of proofs.
 
> Yes, it might indeed be impossible to objectively draw
> the *exact* line between the absolutely certain
> mathematical propositions, and those which are
> less-than-absolutely-certain. Indeed, I do not pretend
> that I know where the exact line is.

It is likely that there is no exact line. There is only a relative kind of
certainty. Or perhaps a few particularly robust exact lines.

> But even without exact line
> there are obvious cases  of the two sorts. Thus the fact
> that there are infinitely many primes was absolutely
> certain at the time of Euclid, it is still
> absolutely certain today, and so it will  remain forever.

I don't see why. There is clearly a distinction between "there are
infinitely many primes" and "there are at least 100 primes" on many
important levels. 

> The same applies (since 1931) to Godel's incompleteness theorems.

I don't like this example, because there is no agreed upon exact statement
for some of them - opening up an entirely new but vitally important kind of
issue.

> In contrast, it should be obvious that
> neither GCH nor its negation will ever be
> recognized as absolutely certain.

I wouldn't say "obvious", but there are certainly many many surprising
events that must occur before this happens, none of which are on the
horizon.

> The only way to change
> the status of a proposition to "absolutely certain" is by
> *proving* it on the basis of absolutely certain axioms,
> using absolutely certain methods of proofs.

Thus you are using "absolutely certain" in a way that rules out Monte Carlo
methods? 

> We know
> that GCH can be decided only on the basis of *new* axioms, and
> by the nature of absolute certainty, no proposition
> that was doubtful in the past can suddenly become
> absolutely certain to the point it would deserve full
> acceptance as a certain *axiom* (which does not requires a proof).

I am dubious about this argument. Wasn't there a point before proofs by
induction were accepted, and things had to be proved formally? What about
the history of the certainty of the commutative law of addition for
integers?
> 
> Once we recognize that there are some absolutely certain
> mathematical propositions and some that are not (Of course,
> there will always be strange people who deny it.
> The only thing one can do about it is to ignore them),
> it is important to find out (as far as possible)
> what is the extent and applicability of those who are.
> It is not necessary to find the
> exact line (if such exists). It suffices to determine
> a large body of mathematics that has absolutely
> secure foundations on one hand, and supports the
> most important parts of classical mathematics on the other.
> This is what the predicativist program is all about,
> and I think that a very  strong
> case can be made that not only has it succeeded,
> but also that it is the only current approach
> that does work,  and does achieve the primary goal
> of FOM described above.

At the moment, we only see a scale of certainty. There are always problems
with ultimate meaning and ultimate certainty - at least when one gets past
things that are far far far below what you are referring to.

Harvey Friedman