[FOM] Impredicativity of Kruskal's Theorem

[Harvey Friedman]

On 4/4/06 12:25 AM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:
 
> 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.

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

Much much older than what? I don't see what it is I am supposed to
"retract". 

I wrote

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

When I said "much older" I was referring to Weaver's analysis. I wasn't
aware of any serious analysis until Feferman/Schutte. I still am not. Is
there any such serious analysis?

Weaver says that Wang and Lorenzen, earlier than Feferman, took views on
predicativity that are more liberal than Feferman/Schutte.

I have my doubts that they expressed any coherent well worked out idea that
is relevant to my opinion that Feferman/Schutte is much much older than any
coherent competing idea.

In fact, Weaver said this about Wang's position:

"Hao Wang considered the question of which ordinals are
predicatively acceptable, and tentatively proposed an answer:
the predicative ordinals are precisely the recursive ordinals.
Wang's idea was that (1) there is no predicative difficulty
in defining all recursive well-orderings of omega and (2) by a
result of Spector, no non-recursive well-ordering of omega
will appear in L_\alpha for any recursive \alpha.  Thus, the
predicativist can access all recursive ordinals but will never
be able to reach any non-recursive ordinal."

This is a very early idea of Wang that was rejected immediately (or should
have been) as being naïve and incoherent on many grounds. In particular, we
know that it is not proof theoretic, and does not grapple at all with any of
the serious issues. This is before researchers, generally, were entirely
comfortable with various subtleties of higher recursion theory (hyp sets, H
sets, recursive ordinals, etc.). So it is entirely irrelevant to the
discussion.

As for Lorenzen, I would like to hear more. What coherent ideas on this did
he really put forth? If what you wrote about Wang is representative of
Lorenzen, then he certainly did not.

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

I said this because 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".
 
> 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.

It is not a tautology. The number of (reasonably informed, relevant) people
who, like you, think that "there is a single coherent notion of
predicativity", now in 2006, is what? I would guess that it would be less
than 5 worldwide. Of course, there are a lot of relevant people who neither
believe this nor believe its negation. And of the five, the number who
promote a special analysis of predicativity - and that includes you, even if
it is not a complete analysis - is what? OK, if it's not 5, then maybe it's
4. I stand corrected (smile).
 
>> 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?

It shows the sharp contrast between "predicativity" and "effectivity". This
is a very important point.

> 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 am glad that you use the word "seem". I don't even know what you mean by
"defect" in the first sentence above.

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

It doesn't trouble anyone else that I know for these reasons.

1. There is no convincing defect.
2. Although there are weak points that can be complained about, this is true
of any (what you call) "foundational stance".
3. So in light of 1,2, people prefer to obtain significant results using the
measuring rod of the canonical hierarchy of natural formal systems.
4. When there are, historically, sufficiently controversial differences,
then one may be compelled to start using names as adjectives. Like Brouwer
constructivity versus Bishop constructivity, or Tait finitism versus Kreisel
finitism. Granted, these are not in fully common use.
5. In particular, it is generally considered counterproductive to dwell
endlessly on the right or wrong of Brouwer versus Bishop, or Tait versus
Kreisel. 

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

Again, the reason for this is that almost no one thinks that the words
"predicative" provide much more than a rough outline of what is or is not to
be admitted. So the attitude is that there is green predicativity, blue
predicativity, red predicativity, orange predicativity, etcetera.

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.

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

Impossible. The people you are talking about will be mathematicians, and
mathematicians immediately would adopt the exact same view that I have. They
would simply say that all of this fuss is purely a matter of terminology.
And terminology is not interesting.

You don't have much of a chance for "reform" with people in mathematical
logic. Your only chance would be a certain kind of philosopher. But there
that is highly unlikely in that your approach to the issues is so technical.
> 
> 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.  

I repeat that 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).

I do not believe that Poincare or Weyl would have considered Gamma_0 to be
OK, and certainly they would have rejected KT.

Now, they might have disavowed predicativity entirely when they see some of
the jewels that you lose. They look fundamental, and have the feel of being
the tip of the iceberg.

And what "people" are you talking about? Where do you find all these
mathematicians outside logic that venture opinions about Gamma_0?
> 
>> 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.

You are absolutely correct. So in real life, predicative versus
nonpredicative, for me, is a black and white issue that doesn't require any
deep analysis. 

By the way, I am so dubious that "predicativity" has any clear unique
meaning, that I am also not convinced that gamma_4 is predicative - even
though it is under the Feferman/Schutte analysis.
> 
> 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.

And apparently thinking deeply about it doesn't help either - at least in
the sense of convincing people with different views, or decisively
determining whether gamma_4 is predicative or Gamma_0 is predicative. The
notion "predicative" starts to seriously split.
> 
>> 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.

People are so unconvinced of any one meaning of "predicative" that they are
going to rightly view your claim above as dogmatic.

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

And because nothing sounds better. F-S is a very clear identifier now.
Certainly, if something cannot be proved in F-S then something exotic
foundationally is happening - that, e.g., Poincare and Weyl would have been
deeply moved by.
> 
>> 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.
> 
>> 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.  

You should want to analyze why what I say is true. The answer is that people
just don't believe that "predicativity" has enough right and wrong in it.
And any fixed target can be complained about.

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

Since it is in the four-sentence abstract, it is "apparent".
> 
>> 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".

There is no proof of Kruskal's theorem there.

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.

This has the general look and feel of setting up a technical formalism and
trying to claim some special significance for it by simply declaring it to
be predicative. As I said many times, there is nothing in the word
"predicative" that is going to make people convinced that there is anything
in Weaver to be preferred to Feferman/Schutte - or even that there is any
defect in Feferman/Schutte that should compel us to change historical
terminology.  

So the obvious reaction is simply that there is

Feferman/Schutte predicativity
Weaver predicativity

with Feferman/Schutte having been accepted for over 40 years, and being a
fixed target. Weaver predicativity dates from its date of publication(?),
and is NOT a fixed target. At this point, it just has the look and feel of a
complaint about historical terminology.

Harvey Friedman