[FOM] Impredicativity of Kruskal's Theorem

[Nik Weaver]

I corrected Harvey Friedman's comment that the Feferman-Schutte
analysis of predicativism is "much much older" than the view
that generalized inductive definitions are predicative.  He
responded:

> 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.

So, do you retract your claim about the Feferman-Schutte analysis
being "much much older"?  I assume so, but you don't say.

This sentence takes a little effort to parse, but basically
(removing the double negative) you seem to be saying "the
only people who believe there is a single coherent notion of
predicativity are those who promote a special analysis of
predicativity."

This is almost a tautology, but not quite --- and it's false.
I believe there is a single coherent notion of predicativity,
but I do not promote a special analysis of predicativity, at
least not in the sense of believing there is a special formal
system that exactly encapsulates predicative reasoning.  I
have told you this several times.

If we interpret "promoting a special analysis of predicativity"
more loosely as "believing there is a single coherent notion of
predicativity" then I am no longer a counterexample, but then
the statement really is a tautology.

> 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.).

Fine, but how does this relate to the question about predicativism?
You *seem* to be insinuating that the failure of predicativism to
be encapsulated in a single formal system should be considered a
defect.  Can platonism be encapsulated in a single formal system?
Can intuitionism?

I recall that you believe there is a hierarchy of philosophical
beliefs which correspond to various natural formal systems.  This
strikes me as pretty artificial.  I like these formal systems too
but the real foundational stances that people actually believe
don't seem capable of being put in neat boxes like this.

> 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.

The fact that the F-S analysis has been almost universally accepted
for over 40 years indeed troubles me.  Initially it may have seemed
new and interesting and, if one didn't think about it too closely,
likely correct.  However, over time its flaws should have become
apparent and one would have expected a more nuanced understanding
to develop.  Instead, it looks as though the foundations community
has adopted a completely uncritical attitude toward the question.
People like the simple answer given by F-S and don't want to think
about it any more, apparently.

What would be even more disturbing would be someone from another
field noticing the difficulties, thoroughly researching the question,
and writing a paper spelling everything out in great detail, and for
the foundations community to still not accept the correction.  No
matter how you spin it I think that would reflect very badly on
the field.

As to the F-S characterization doing a "great job" in reflecting
what is intuitively recognized as predicative, I just don't think
it does.  In my experience most people intuitively think Gamma_0
looks like it can be "built up from below" and so do substantially
larger ordinals.  Robin Gandy: "one may suppose that even Poincare
... would have accepted the proof of TI up to Gamma_0" (Math Reviews
# 0193006).

> 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.

Well, if the criterion has to do with easily understood proofs
that don't involve logic you hardly need to go up to Gamma_0.  I
doubt you can give a single example of an intuitively predicative
proof that is not completely artificial and which needs ordinals
beyond, say, gamma_4, where (gamma_n) is the canonical sequence
whose limit is Gamma_0.

However, that is not a good criterion.  The correct criterion is:
what kinds of reasoning respect the intuitive requirement that
circular constructions must be avoided?  That's something you can
only answer by thinking about it deeply.  Two-dollar experiments
where you ask random people what they think won't tell you much.

> 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.

It is not a different interpretation.  I have said this several
times already.  It is a corrected analysis under the same
interpretation.

> 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.

Are you not aware of Russell's role as a founder of predicativism?

So there's no objective right or wrong, but we should stick with
the F-S characterization for the sake of tradition and because it
sounds good if you don't think about it too hard.  Is that a fair
summary of your view?

> 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.

You haven't read my criticism.  It is highly specific to the
case of predicativism and Gamma_0.

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

That's a cheap shot, and it reflects more badly on you than it
does on me.  Indeed, comments like this:

> but apparently Weaver claims that
>
> KT is predicatively provable under the Weaver analysis.

show that you don't know what my analysis says.  My analysis is
contained in my paper "Predicativity beyond Gamma_0" and I already
say in the four-sentence abstract that phi_{Omega^omega}(0) is
predicatively provable (which implies that KT is predicatively
provable, as you well know).  So I gather you haven't even read
the abstract of my paper.

> 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 ...

See Section 2.10 of "Predicativity beyond Gamma_0".

Nik Weaver
Math Dept.
Washington University
St. Louis, MO 63130 USA
nweaver at math.wustl.edu
http://www.math.wustl.edu/~nweaver/