[FOM] predicative foundations?

[Harvey Friedman]

Avron wrote:

> why not choosing a good point
> which is *not* arbitrary (like predicative mathematics) and devote
> most of our efforts  to it? or at least wait until "core mathematicians"
> come themselves across problems in which they need stronger methods,

This is not suitable for the currently accepted main purpose of f.o.m. - to
study "mathematics and mathematical practice as scientific phenomena", for
these reasons (and more):

1. Mathematicians will not adhere to any explicit formalism. Currently they
(the community as a whole) implicitly adheres to ZC, which is ZFC without
replacement. 

2. Mathematicians (as a community) certain would never even consider
adhering, implicitly or explicitly, to any complicated or clumsy formalism.

3. Core mathematicians have already come across Kruskal's theorem and the
graph minor theorem, and awarded prizes for the latter. Under a strict
definition of core mathematics, these theorems may not be admitted, although
they are respected.

4. I have no doubt that one can apply these theorems in an essential way in
strictly core mathematics.

For these reasons alone, a single minded focus on predicative foundations
for f.o.m. is unwarranted, and will not properly treat "mathematics and
mathematical practice as an object of study".

Predicativity is one of many not unreasonable "stopping places" in an
extensive hierarchy of logical strengths from EFA through j:V into V.
Current conventional wisdom is that the informal notion of "predicativity"
is not sufficiently sharp to correspond to a single place in this hierarchy.
So there is a serious question as to how natural a place it is to single out
instead of many other places.

John Steel gives a different reason for rejecting a single minded focus on
predicativity.
 
> As I understand it, predicative mathematics is not such a "good point", as
> the existence of least upper bounds for arbitrary sets of reals is not
> predicatively justified. Not many would want to revamp the way we teach
> undergraduate Analysis in a way that paid attention to predicativity.
> Certainly not our revered "core mathematicians".  So "core mathematicians"
> (whoever those people are-- the editors of Annals of Math?), who have
> learned the naive lub principle, are forever in danger of using it in a
> necessary way.

Avron responds:

> One side remark: in *my* version of predicativism every bounded *set* of
> reals does have an lub, since in this version the union of an "acceptable" set
> is itself "acceptable". What is constrained is the notion of an
> "acceptable" set to which one can apply this principle.

I have my doubts that one can coherently have a simple, transparent
formalism whose logical strength is that of predicativity, and reflects
predicative thinking, where "every bounded set of reals has a lub" - at
least if it is going to be reasonably compatible with mathematical practice.
Mathematicians work with open, closed, F_sigma, and G_delta sets of reals,
and they want G_delta sets of reals to mean what they think it means.

> Now in "our efforts" I meant not the "core mathematicians",
> but mathematicians who are doing research in FOM.

f.o.m. focuses on the study of "actual mathematics and actual mathematical
practice as phenomena".

Certainly there are old fashioned views of f.o.m., going back to Hilbert
(and perhaps earlier) concerning trying to "establish the correctness of
mathematical methods".

However, in light of Godel's work and subsequent developments, this view of
what f.o.m. is has been discarded.

This view may come back if there were a breakthrough that we cannot
anticipate at this time.

But for now, and for quite some time, there appears to be

1. A robust hierarchy of logical strengths ranging from about EFA to about
j:V into V.

2. There has never been any convincing argument that some particular place
to stop in this hierarchy has such a special status to be called "absolute
certainty" whereas above it, or even quite a bit above it, is to be called
"not absolute certainty".

3. A case in point is predicativity. This view takes natural numbers and
sentences in the semiring of natural numbers as "absolutely certain" (or
absolutely certainly false). However, people write about how this conception
of the natural numbers is already "impredicative".

4. Take the usual polemics against the objective meaning of "arbitrary
natural numbers". This appears to be no more or less attractive as an
ideology than the predicativist position.

5. Furthermore, it also appears extremely interesting to study absolutely
finite models of the mathematical universe, such as the first 8 power sets
of the empty set. I wrote about this on the FOM some time ago, discussing
just how much math can be done, and need for almost no axioms. (This does
not readily fit into the hierarchy starting with EFA, as the hierarchy
starting with EFA takes for granted the notion of 'arbitrary natural
number'). 

6. In short, ultrafinitism (see 5 above), and finitism are at least as
interesting a stopping place as predicativity. By default, finitism can be
viewed as more certainly certain than predicativity, and ultrafinitism can
be viewed as more certainly certain than finitism.

7. In fact, foundations of ultrafinitism is the least explored of these, by
far, and seems to me to be a much more interesting "starting point" for many
purposes than predicativity. They both involve, to varying extents,
"reforming" or "recasting" existing mathematics.

Avron continues:

>Also Hilbert did not intend in his
> program to convince "core mathematicians" to use only finitary
> methods. On the contrary: his goal was to allow them to safely use
> their infinitistic methods with full justification. This is
> how I see the main task  of the research in FOM.

This was the current view decades ago. But now we know, solidified through
reverse mathematics, that there is a real hierarchy of logical strengths
corresponding to mathematical practice, and one is not going to "justify"
higher things by lower things.

>It is *our*
> task to find out what is the degree of certainty of various
> pieces of mathematics.

Again, an idea from the past. There is no prospect, short of an unexpected
breakthrough, for assigning "degrees of certainty" to mathematical methods.

A linear order - yes. Just as in the robust hierarchy of logical strengths I
continually allude to.

>It is true that I identify "predicative mathematics"
> with "absolutely certain mathematics", but I think I have
> made it clear that in many (most?) applications one does not need
> absolute certainty.

This identification is completely unwarranted. Justify it if you can.

>Moreover: it is very legitimate to do mathematics
> which is not absolutely certain, as long as it is acknowledged
> that it is  not absolutely certain.

How do you propose that this be acknowledged?

I see no basis for drawing a line of "absolutely certainty" somewhere in the
midst of actual mathematical practice. I don't see any justification for it.

To me, "absolutely certain" means "nothing whatsoever is more certain".

PERHAPS (only perhaps) one can, very very carefully, construct such a
concept - but it would apply very very low down, perhaps where there are,
say, only p objects in the mathematical universe, where p is, perhaps, a few
hundred. In any case, this is way way way below predicativity, or even
finitism or even ultrafinitism.

>Moreover: again it is
> our (the FOMers') tasks to
> determine the degree of certainty of various mathematical
> theorems and methods.

Incorrect, and hopeless, at least today. A liberal interpretation of this
is, of course, RM = reverse mathematics.

>Thus I see the work on reverse mathematics
> as very interesting and important, because I see it as making a
> big progress in this direction.
> 
Not true if "degree of certainty" is what I think you mean. Instead, RM is
big progress in the study of "mathematics and mathematical practice as
phenomena".

Harvey Friedman