[FOM] What would Weyl do?

[Harvey Friedman]

On 2/6/06 9:31 AM, "Stephen Pollard" <spollard at truman.edu> wrote:

http://www.cs.nyu.edu/pipermail/fom/2006-February/009698.html

> Here are some observations and speculations about how Hermann Weyl might
> have reacted to Harvey Friedman's results.
 
> In sum: The early Weyl would not have accepted utility as a reason for
> employing classical set theories. The early Weyl did accept utility as a
> criterion for choosing between predicative set theories. The later Weyl
> might have accepted utility as a reason for employing theories on the
> borderline of evidentness.
> 

It is known that one can adjust parameters in Kruskal's theorem to hit many
levels of logical strength at or below Pi12-TI0, with the help of labels
from finite sets. 

The most natural striking examples I can point to are as follows.

1. Kruskal's theorem for binary trees is equivalent to "epsilon_0 is well
ordered" over RCA0

2. Kruskal's theorem for binary trees with two labels is equivalent to
"Gamma_0 is well ordered" over RCA0.

In http://www.cs.nyu.edu/pipermail/fom/2006-February/009698.html an
intermediate system somewhat higher than ACA in logical strength is
discussed as an option that Weyl considered but rejected as "useless".

There should be a natural theorem from wqo theory that would correspond to
the system Weyl considered but rejected as "useless".

Of course, the significance of the work on Kruskal's theorem and the graph
minor theorem does not depend on the "correct" interpretation of the views
of these important mathematicians, or others.

Rather, it is basic information that obviously affects at least some
reasonable views -  in fact, views that are held by reasonable people.

Specifically, there is the reasonable view that the issue of the extent of
predicativity makes no difference for mathematical practice. E.g., that once
one focuses on "predicatively meaningful theorems", all interesting
mathematics is well within weak fragments of predicativity.

This is decisively refuted by the work on KT and its weakenings.

NOTE: One can complain that KT is itself not "predicatively meaningful",
since it has a universal quantifier over all infinite sequences. Of course,
one has to reconcile this objection with the fact that one cannot even do
undergraduate real analysis in any usual sense without quantifying
universally over the real numbers. NEVERTHELESS, one can meet this objection
to the work on KT as follows.

a. One can go to the various finite forms. See my paper in the volume
dedicated to Feferman published by the ASL.
b. More satisfactory even than this, from SOME points of view, would be to
simply restrict KT to all "predicatively given" or even "effectively given"
infinite sequences of trees.

In both cases, the resulting sentence is not predicatively provable under
the Feferman/Schutte analysis.

*********************************

Despite this, the view can be resurrected replacing "mathematical practice"
with "core mathematical practice" with the intention of eliminating KT as
not core. 

I find it very interesting to take this modified view seriously -
independently of the fact that I do not find it attractive. So there remains
the challenge of doing something decisive with this modified view. Even that
will be accomplished decisively at some point, in a very interesting and
productive way.

Thus, when I do this kind of work, I remain agnostic about the various
underlying positions that can be taken.

QUESTION. What would other historical figures do? E.g.,

Poincare, Lorenzen, Hilbert do?

Harvey Friedman