[FOM] Impredicativity of Kruskal's Theorem

[Harvey Friedman]

On 4/1/06 8:25 PM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:

> 
> Harvey Friedman wrote (quoting Bas Spitters):
> 
>>> "Predicativity" as used by Feferman-Schutte refers to a level of
>>> proof-theoretic strength. By type theorists the term is used for
>>> a kind of "non-circularity in definitions" ...
>> 
>> I strongly recommend, for historical and other reasons, that people
>> refrain from using "predicative" for anything not falling under the
>> scope of the much much older and classically accepted analysis of
>> Feferman/Schutte.
> 
> Friedman is way off here.  To the contrary, the idea that
> generalized inductive definitions are predicative is actually
> older than the Feferman-Schutte analysis.  I don't know if it's
> "much much older" but it is clearly enunciated in, for example,
> H. Wang, "The formalization of mathematics", JSL 19 (1954),
> 241-266 and in P. Lorenzen, "Logical reflection and formalism",
> JSL 23 (1958), 241-249, both of which appeared well before
> Feferman's first paper on predicativism in 1964.

I know of no one who doesn't have a special analysis of predicativity that
they promote who believes that there is a single coherent notion of
predicativity that has any kind of uniqueness to it. This is in sharp
contrast to effectivity, where the vast majority of people who don't have
any special analysis (very few do), believe that there is a single coherent
notion (modulo the proviso that one is not talking about physical processes,
and one is talking about no limitations on resources, etc.).

So since the Feferman/Schutte analysis is by far the most well known and
well worked out and well accepted analysis, for over 40 years!, and since it
does such a great job in reflecting what mathematicians immediately sense is
an impredicative definition, there is no point in abandoning the current
practice of adhering exclusively to Feferman/Schutte in connection with
predicativity. 

In particular, I do not know of a single case where a proof has ever been
presented to any mathematicians outside logic, which in fact was done
impredicatively under the Feferman/Schutte analysis, where the
mathematician, upon a brief explanation of what in impredicative definition
is, didn't immediately see that the proof was impredicative. I have
certainly done experiments like this, and they all came out this way.

If people want to talk about

Weaver predicativity

than that is reasonable, as long as they explain that this is a more liberal
interpretation of predicativity than Feferman/Shutte, and is not generally
accepted, and comes more than 40 years later.

Feferman/Schutte predicativity.
> 
> Could Friedman describe his "other reasons" for insisting that the
> term "predicative" be used not to refer to the actual foundational
> stance of that name originally developed by Poincare and Russell,
> but rather to a particular attempt at formalizing that stance which
> has recently come under severe criticism (by me)?

The actual foundational stance of Poincare and Weyl and whoever you put in
this category (Russell??) is obviously subject to subjective interpretation,
and it is inconceivable to almost everyone who doesn't have a stake in their
own subjective interpretation, that there is any objective right or wrong
here. To declare that there is, at least in this case, is to misunderstand
the foundational situation.

>Does he have
> anything to say about that criticism, which I claim reveals a basic
> flaw in the original Feferman-Schutte analysis involving a confusion
> between induction and recursion?

Any analysis of anything even remotely like predicativity - e.g., finitism,
ultrafinitism, constructivity, etcetera, is subject to the same kind of
criticism, and the same kind of failed attempts by some people to claim a
superiority over other people's analyses. I.e., where do you stop? Weaver
attempts to claim such a superiority, and is apparently unusually forceful
in his view of this superiority.

>How does he justify his continued
> reference to Kruskal's theorem as being predicatively unprovable in
> the face of my thorough analysis of predicativism which I claim
> shows that Kruskal's theorem is in fact predicatively provable?

KT is predicatively unprovable under the Feferman/Schutte analysis. I for
one, and people generally, are not concerned with the Weaver analysis, but
apparently Weaver claims that

KT is predicatively provable under the Weaver analysis.

I don't see the interest in this, since we do have the gold standard. Namely
the canonical hierarchy of logical strengths, and we know exactly where KT
fits.

I suggest that Weaver present a proof of KT that he thinks is predicative,
and readers can judge for themselves whether or not it is predicative, or,
like me, would, when presented with such a proof, perhaps simply say that it
is predicative under the Weaver analysis, and leave it at that. So, can
Weaver show us a real mathematical proof of KT that is predicative?

The full KT - which is KT with labels - is discussed in my posting number
275, which should come out today. This is obviously impredicative, and is
what Kruskal really proved, and is proved in the course of every natural
proof that I have ever seen given for KT.

Harvey Friedman