[FOM] Impredicativity of Kruskal's Theorem

[Nik Weaver]

Harvey Friedman rejects my suggestion that he retract his
claim that the Feferman-Schutte analysis of predicativism
is "much much older" than the idea that generalized inductive
definitions are predicative.  He writes:

> I don't see what it is I am supposed to "retract" ... When
> I said "much older" I was referring to Weaver's analysis.

Well, here is the original exchange between you and Bas Spitters:

> > 2. "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", as it
> > was used originally by Russell. Martin-Lo"f's type theory with
> > enough inductive definitions is "impredicative" according to
> > Feferman. In this sense one can say that there is a "predicative"
> > (ie non-circular) proof of the extended Kruskal theorem.
>
> 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.

You weren't referring to my analysis.  You were referring to
Spitters' reference to generalized inductive definitions as being
predicative.  This was in the context of a discussion that didn't
mention me and is orthogonal to my position.

> ... you promote a special analysis of predicativity, that you
> claim is sufficiently powerful to "refute" the Feferman/Schutte
> analysis. Since you leave it open ended, your analysis is not
> sufficiently powerful to determine other "properties of
> predicativity".

My critique of the F-S analysis is distinct from my alternative
proposal involving hierarchies of truth predicates.

I have no idea what the second sentence is supposed to mean.
"Properties of predicativity"?

> > Fine, but how does this relate to the question about
> > predicativism?
>
> It shows the sharp contrast between "predicativity" and
> "effectivity". This is a very important point.

I'll ask again.  What point were you trying to make by interrupting
a discussion of predicativism in order to make an irrelevant comment
about effectiveness, and why do you now inform us that the non-relation
between predicativism and effectiveness is "a very important point"?

> > I recall that you believe there is a hierarchy of philosophical
> > beliefs which correspond to various natural formal systems.
>
> I would not assert this statement.

Here's what you wrote in an earlier message:

> On can stop a lot earlier than "predicativity", say, stop at ACA0
> or RCA0, or one can stop somewhat higher than "predicativity", say
> at one inductive definition, or Pi11-CA0. Or one can stop even
> higher at, say, the theory of a recursively inaccessible, or what
> have you.
>
> All of these stopping places, and many more, have very "nice"
> stories. All of these stories have advantages and disadvantages.
> These advantages and disadvantages make sense and have their
> proponents, both mathematically and philosophically.

Have you changed your mind about this?  Or do you draw some
significant distinction between a "philosophical belief" and
"a story which makes sense philosophically and has philosophical
proponents"?

> 1. There is no convincing defect [in the F-S analysis].

Until you've read and understood my critique, merely asserting
this doesn't add much to the debate.

> And if you persist long enough and write enough papers that are
> published in good Journals and those papers are sufficiently
> attractive to read and have students who also promote your view,
> then, over time, people will simply say that there is Feferman/
> Schutte predicativity, and there is Weaver predicativity.
>
> But since you do NOT propose any kind of closed ended system for
> predicativity like Feferman/Schutte, they really can't even call
> it Weaver predicativity. So people will then simply refer to
> Feferman/Schutte predicativity, and that's all. Period.

It's funny you should say that, because just a few sentences
earlier you were talking about Brouwer constructivity and Bishop
constructivity.  I don't think either of them proposed any kind
of closed ended system.  So this pronouncement is not well-taken.

As to your predictions about the future, another possible chain
of events is that as new logicians and philosophers who have not
committed themselves to the F-S analysis enter the professional
world, you will see a gradual steady increase in acceptance of
my position as a correct interpretation of the informal notion
of predicativism, together with a gradual steady decline in
support for the F-S analysis.

> > What would be even more disturbing would be someone from
> > another field noticing the difficulties ...
>
> Impossible. The people you are talking about will be
> mathematicians, and mathematicians immediately would adopt
> the exact same view that I have.

Are you still not aware that I am a mathematician?  I've mentioned
it several times.  I'm a C*-algebraist.

> > > 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.
>
> Not really. Tait has said that finitism is encapsulated by PRA.
> But you can see the Ackermann function from below. Tait has a
> defense, and Kreisel can attack again. And so forth. The details
> are always different, but the flavor is always the same.

Yes, really.  Please stop making claims about the nature of my
critique until you've read it.

> Since it is in the four-sentence abstract, it is "apparent".

You wrote "but apparently Weaver claims that KT is predicatively
provable under the Weaver analysis."  I said that your uncertainty
about this revealed a lack of familiarity with my work: if you had
read only the brief abstract of my paper, you would know this.

Your rejoinder does not help your case.

> I, or any number of people, can give the beautiful purely
> mathematical proof of KT due to Nash-Williams. And we can
> examine that proof to see whether or not it is predicative,
> and why.
>
> Why doesn't Weaver give a nice mathematical proof of KT that
> we can judge for ourselves is or is not predicative? More
> specifically, so that we can judge for ourselves whether or
> not Weaver's claim that it is predicative is compelling?
>
> Instead, there is merely a long winded and rather technical
> development that one can prove that theta_Omega(0) is well
> ordered in some technical formal system with a long winded
> dogmatic development claiming that that technical formal
> system is really predicative - despite its not falling under
> the Feferman/Schutte analysis.

Certainly the standard proof is impredicative.  But that is not
your claim.  Your claim is that there is *no* predicative proof.
This comes down to a claim about which ordinals are predicatively
provable, a reduction due to Rathjen and Weiermann.

Simple obviously predicative systems have very small proof-theoretic
ordinals and are not strong enough to prove Kruskal's theorem.
However, we have the ability to apply reflection principles and
bootstrap up to stronger systems using, for example, the fact
that we recognize the original system is consistent.  The key
insight behind my predicative well-ordering proofs is that this
form of reasoning can be powerfully organized within formal
systems that employ a hierarchy of truth predicates.  This
appears to be the most effective technique for bootstrapping
up to relatively strong systems which can prove that notations
for relatively large ordinals are well-ordered.

The details are provided in my paper "Predicativity beyond Gamma_0".
Your call for "a nice mathematical proof of KT" that is predicative
is pointless.  The question is which ordinals are predicatively
provable, and I have analyzed that question in great detail.  Your
crude dismissal of this analysis ("long winded" and "dogmatic",
terms that might indeed be applied to your own writing) establishes
nothing.  Can you find any circularity in it?  That's the relevant
question in determining predicative legitimacy.

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