[FOM] predicativism and functional analysis

[Harvey Friedman]

On 2/22/06 10:35 PM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:

Weaver is replying to Bas Spitters
http://www.cs.nyu.edu/pipermail/fom/2006-February/009988.html

who argues that formalization of the bulk of functional analysis can be done
at the level of PRA.

Furthermore, Spitters states that the result of Kohlenbach's work on showing
that PRA is "usually sufficient" had consequences for Kohlenbach's work on
data mining to get hard core information of a new kind that is apparently
valued by experts. 

Spitters cites Kohlenbach's forthcoming book

Proof Interpretations and the Computational Content of Proofs
http://www.mathematik.tu-darmstadt.de/~kohlenbach/newcourse.ps.gz

Weaver asserts that predicativity can do more functional analysis than the
PRA level, but apparently concedes that the difference is not substantial.

So I view Spitters as, in my words, "objecting to predicativity from below".

The objections to predicativity from above are also very substantial.

1. Grothendieck universes and topoi for FLT and apparently even concrete
algebraic geometry. Substantial work is expected to eventually show that
this is not needed. But the fact that mathematicians currently do things
this way already shows just how well set theory fits into mathematical
practice. 

2. The work of functional analysts in Paris, Debs and Saint Raymond, and the
spin off for Borel selection that uses, NECESSARILY, uncountably many
uncountable cardinals.

3. Kruskal's theorem and the graph minor theorem.

4. Boolean relation theory. Certain to become accepted normal mathematical
activity when digested. Over the long haul, will certainly become core
mathematical activity.

5. Emerging work in finite graph theory. Finite graph theory is definitely
core mathematical *activity*, if not core mathematics - as evidenced by the
fact that graphs are the most basic mathematical structures in the discrete
sciences. 

6. Of course, there is the unabashed use of the least upper bound principle
all through the educational process and in mathematical papers.

7. Highly impredicative Zornifications in countable algebra - even in
finitely generated structures.

So, just as I have been emphasizing all along, predicativity - like every
other ivity not at the bottom or top - has serious objections from below AND
from above. 

In order to dodge these objections, one has to carefully say just what
mathematics is being considered and just what mathematics is rejected for
consideration. One must walk a very fine line.

Much better to abandon this idea of a "special place" for predicativity.

The real item is the robust hierarchy of logical strengths from EFA through
j:V into V. 
 
> Whether PRA "suffices" seems debatable.

How about ACA0? Does that clear up all of the problems you cite? Bigger than
PRA, and corresponding to PA.

> Predicativism doesn't suffer from these defects, but there are
> still going to be occasional topics out at the margins that won't
> be allowed.  So it's a matter of degree.

MATTER OF DEGREE! Thank you for now agreeing with me. There is a robust
hierarchy of logical strengths, and no brand of "predicativity"  - Gamma_0
or somewhat higher - has any particularly special place.

> I still maintain that the
> correspondence between predicativism and core functional analysis
> is stunningly exact.

Would it be stunningly exact if ACA0 does the same job? The answer to that
is no. Does ACA0 do the same job?

>The correspondence with constructivism is
> pretty good but you're missing a few things that people really care
> about.  

Sounds like you agree with me that "predicativity" doesn't have any special
place. 

>The correspondence with set theory is terrible because the
> interesting objects are buried in an ocean of uninteresting,
> pathological objects.

"The correspondence with predicativity is terrible because the interesting
objects are buried in an ocean of uninteresting, pathological objects".
After all, almost all integers are uninteresting and pathological. Same for
recursive sets of integers. Same for separable Banach spaces. Almost all
separable Banach spaces are uninteresting pathological objects.

I make the above argument to show how dubious your dogmatism is.

Harvey Friedman