[FOM] Impredicativity of Kruskal's Theorem

[Harvey Friedman]

First of all, there seems to be agreement with Weaver on this:

Labeled Kruskal's theorem (proved by J.B. Kruskal in his paper that first
proved Kruskal's theroem) is not predicatively provable on any proposed
analysis of predicativity.

CORRECTION: In http://www.cs.nyu.edu/pipermail/fom/2006-April/010337.html I
wrote that Higman's theorem corresponds to labeled Kruskal's theorem for
bounded valence. It depends on which Higman's theorem (involving
divisibility orders) we are talking about. The situation is like Kruskal's
theorem, in that the most basic one corresponds to Kruskal's theorem for
bounded valence, whereas in the same place a more general version is also
proved which corresponds to labeled Kruskal's theorem for bounded valence
(impredicative). 

On 4/7/06 4:02 PM, "Nik Weaver" <nweaver at math.wustl.edu> wrote:

Bas Spitters wrote:
> 
>>> 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", ...

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

I reiterate this recommendation, and when I wrote it, I had in mind both the
recent use of the term by type theorists discussed by Spitters, but also use
of the term by Weaver.

As far as I know, any formal analysis of predicativity (in the sense under
discussion) older than Feferman/Schutte - to the extent that there are any -
are far less inclusive than Feferman/Schutte. In Russell, one has something
far weaker, without the axiom of reducibility, but with the axiom of
reducibility, which Russell regarded as essential for the use of his
approach in the formalization of mathematics, it is no longer an analysis of
predicativity. 

Weaver has mentioned Wang and Lorenzen. Clearly Wang is not an analysis of
predicativity at all, as I discuss earlier.

I looked at 

S. Feferman, Predicativity, In The Oxford Handbook of Philosophy of
Mathematics and Logic (S. Shapiro, ed.), Oxford University Press, Oxford
(2005) 590-624. 

to see what he says about Lorenzen. Here is what I found, page 28:

"Are those the only two senses of predicativity to be considered? In one
direction, stronger notions of predicativity than that, given the natural
numbers, were suggested by work in the late 1950s of Paul Lorenzen, John
Myhill and Hao Wang. In particular, the paper of Lorenzen and Myhill (1959)
involves the acceptance in a certain constructive form of the countable
ordinals and of inductive proof and definition on them. In metamathematical
terms, their principles would legitimate a system of strength at least that
of ID1, the theory of one generalized inductive definition."

So Feferman regards Lorenzen NOT as an analysis of the "sense of
predicativity" that Feferman is analyzing with Schutte, but RATHER as an
analysis of a different "sense". E.g., for Feferman, Lorenzen (with Myhill)
is NOT a competing analysis of the same notion of predicativity. I adopt
Feferman's viewpoint on this.

Rather than retract what I recommended, I reiterate what I recommended.

In particular, Weaver is giving some sort of complicated open ended analysis
of another notion of predicativity, which he should rename.

Friedman wrote:
 
>> ... 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".

Weaver wrote:

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

By other properties, I mean, for example: does it or does it not prove the
extended Kruskal theorem (EKT), or the graph minor theorem. You cannot
decide this because of the open ended nature of your analysis.
 
Weaver wrote:

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

This is an essential point. With "effectivity" there is general agreement
that there is a single notion to be analyzed - at least provided one adds a
few choice words. E.g., effectivity, independent of the size of resources
involved, as long as they are finite and deterministic, and not dependent on
physical processes.

There is absolutely no such general agreement that there is a single notion
of "predicativity" to be analyzed. It is very rare to hear about someone who
thinks so. In fact, a substantial percentage of experts in logic think just
the opposite. I am one of them.

I am a bit unclear on this point, but think that Feferman is also one of
them in the vast majority.
> 
Friedman wrote:

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

I have looked at enough materials, including from Feferman, to draw this
conclusion. Your simply pointing to your paper and not making a convincing
case on the FOM also does not add much to the debate.

Friedman wrote:
> 
>> 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.

There is a big difference. There is already for over 40 years a very well
accepted analysis that IS closed ended. You are trying to attack this very
well accepted analysis, effectively trying to replace it with an open ended
analysis. I can't imagine that this is going to be successful.

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

I will grant that this is logically possible. What is almost certain is that
such people will take my point of view on this. That there is not any one
fixed notion of predicativity, and that Feferman/Schutte is an adequate
analysis of one interesting notion of predicativity.
> 
>>> 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.

I looked at your website at http://www.math.wustl.edu/~nweaver/ and saw only
a few logic papers. This confuses me. Why do you emphasize your manuscripts
on logic to the exclusion of C*-algebras on your website?

Friedman wrote:

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

Weaver wrote:
 
> 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.

"Apparently" does not reflect uncertainty. In fact, if something is apparent
then it may well be certain.

Weaver wrote:

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

It is preposterous that there is any single notion of an ordinal being
predicatively provable. This is a derived notion, not a fundamental one.
> 
> Simple obviously predicative systems have very small proof-theoretic
> ordinals and are not strong enough to prove Kruskal's theorem.

And some of them represent alternative notions of predicativity that are
perhaps even more fundamental than the one Feferman/Schutte analyzes, and
the yet other one that you partially analyze.

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

Have the ability? You are obviously trying to informally describe some
notion of predicativity, among the many many ones. In fact, it does not
appear to be a distinctive one among these.

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

Sounds technical, and not fundamental. Seems to be tied to some special
brand of predicativity.

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

For example, show us a proof that YOU call predicative, of the fact that one
of these big notation systems is well ordered. Then we can examine here on
the FOM in what sense your argument is predicative. I suggest you do it
here, as I doubt if anybody is going to look at your complicated paper who
hasn't already.

I suggest that you try to make this as understandable as possible, for
otherwise people are just not going to want to wade through complications.
After all, you are trying to convince people that they have a prior notion
of "predicative" that should apply to your technique.

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

Without a nice simple mathematical proof of KT that is predicative, or some
other critical example, I don't see how you are going to test people's idea
of "predicative" that you claim that they all have in common.

Consider Feferman's letter to you at

http://www.math.wustl.edu/~nweaver/response1.html

that you placed a link from your website:

"I had to laugh when I came to this after trying to wade through your
systems, since here you also blame the failure of the mathematical community
to go predicative on "the awkwardness of predicative systems [of the kind I
have developed] in practice". Wait till they see these systems of yours!"

So you should make your case here on the FOM without making us "wade through
your systems". 

Harvey Friedman