[FOM] 276:Higman/Kruskal/impredicativity

Tue Apr 4 06:31:30 EDT 2006

Here I want to go more deeply into some aspects of the proofs of

1. the Kruskal Theorem.
2. the Labeled Kruskal Theorem.
3. the Extended Kruskal Theorem.
4. the Extended Labeled Kruskal Theroem.
5. the Graph Minor Theorem.
6. the Higman Theorem.
7. the Recursive Kruskal Theorem.
8. Conclusions.

In http://www.cs.nyu.edu/pipermail/fom/2006-April/010308.html I neglected to
take into account seminal work of Graham Higman that is PRIOR to the work of
J.B. Kruskal. This work is clearly impredicative under every proposed
interpretation of predicativity.

I also need to correct a statement I made in
http://www.cs.nyu.edu/pipermail/fom/2006-April/010308.html

1. THE KRUSKAL THEOREM.

The original proof of KT is in

[Kr60] Transactions of the American Mathematical Society, vol. 95, 1960,
210-225.

Kruskal does not use minimal bad sequences (due to [NW], see below), but
instead uses a method which requires proving forms of the labeled Kruskal
theorem, LKT. 

As stated in http://www.cs.nyu.edu/pipermail/fom/2006-April/010308.html we
know that the labeled Kruskal theorem (even for 2 labels) is impredicative
on every proposed interpretation of predicativity yet put forward.

Without any doubt, the simplest proof of KT appears in

[NW65] Crispin St. J. A. Nash-Williams, On well-quasi-ordering infinite
trees, Proceedings of the Cambridge Philosophical Society 61 (1965),
697-720. 

This easiest proof, which is by far the most well known proof, uses the
minimal bad sequence lemma, which is equivalent to Pi11-CA0 (see reference
in my posting #275).

The proof in [NW65] ALSO uses Higman's lemma:

HIGMAN'S LEMMA. Let Q be a wqo. The usual quasi ordering of all finite
sequences from Q is also wqo.

AND, Higman's Lemma is in turn proved, in [NW65], using the minimal bad
sequence lemma, once again!

Subsequent investigations have shown how to prove Higman's Lemma in ACA_0.
In fact, Higman's Lemma and ACA_0 are provably equivalent over RCA_0 - see

[Si99] S.G. Simpson, Subsystems of Second Order Arithmetic, Perspectives in
Mathematical Logic, Springer Verlag, 1999. See page 408.

Of course, the subsequent proof of Higman's Lemma in ACA_0 is much more
involved than the proof given in [NW] using the minimal bad sequence lemma.

In http://www.cs.nyu.edu/pipermail/fom/2006-April/010308.htm I wrote

"ALTHOUGH I have seen (and worked with) proofs of Kruskal's theorem WITHOUT
using the minimal bad sequence lemma, I have NEVER seen a proof of Kruskal's
theorem WIHTOUT proving the labeled Kruskal Theorem, perhaps with bounded
valence."

I need to correct this. There is the published proof of KT in

[RW93] M. Rathjen, A. Weiermann, Proof-theoretic investigations on Kruskal's
Theorem, Annals of Pure and Applied Logic, 60, 1993.
http://citeseer.ist.psu.edu/rathjen93prooftheoretic.html

that doesn't use the minimal bad sequence lemma, and doesn't prove anything
about Kruskal's theorem with labels. It instead uses the reification method.

In fact, this proof is rather elaborate, taken as a whole. One directly uses
a standard ordinal notation system for theta_Omega(0), the so called
Ackermann ordinal. One also has to prove that this standard ordinal notation
system is well founded. This itself is normally done using systems that
extend ATR_0, and so are impredicative under all proposed accounts of
predicativity. 

2. THE LABELED KRUSKAL THEOREM.

LKT was first proved in [Kr60], the same paper where KT was first proved.
Kruskal called it "the tree theorem".

By far the simplest proof of LKT is again in [NW65], where also the simplest
proof of KT is given.

As discussed in http://www.cs.nyu.edu/pipermail/fom/2006-April/010308.htm
labeled Kruskal Theorem already for 2 labels implies ATR_0, and so cannot be
proved predicatively under any proposed interpretation of predicativity.

Where can LKT be proved? For trees of bounded valence, or so called bounded
LKT, the system ACA_0 + pi12-Bi suffices.

We conjecture that LKT can be proved in Pi13-BI. What is the logical
strength of LKT?

3. THE EXTENDED KRUSKAL THEOREM.

I first wrote 

[Fr81] H. Friedman, Independence results in finite graph theory, I-VII,
unpublished manuscripts, Ohio State University, February-March 1981, 76
pages.

where I proved the independence of KT from ATR. I later extended this lower
bound to the Ackermann ordinal. I also worked out finite forms in [Fr81]
with the bound |Ti| <= i + c.

Then I wrote 

[Fr82] H. Friedman, Beyond Kruskal's theorem I-III, unpublished manuscripts,
Ohio State University, June-July 1982, 48 pages.

where I extended Kruskal's theorem to a theorem about finite trees with
labels from a finite set, where the embedding condition is as usual from
Kruskal, except that there is a simple gap condition imposed. This EKT later
played a critical role in the Graph Minor Theorem of Robertson/Seymour.

Simpson wrote an exposition of [Fr81], [Fr82]:

[Si85] S.G. Simpson, Nonprovability of certain combinatorial properties of
finite trees, 87-117, in: Harvey Friedman's Research on the Foundations of
Mathematics, Harrington, Morley, Scedrov, Simpson (editors), Studies in
Logic and the Foundations of Mathematics, vol. 117, 1985.

The proof of EKT involves BOTH the use of the minimal bad sequence lemma AND
a version of EKT with labels from a wqo. In particular, I prove the
extension of EKT that uses labels from a finite set for the nonleaves, and
labels from the given wqo for the leaves.

EKT is provably equivalent, over RCA_0, to theta_Omega_omega(0) is well
ordered. This follows easily from my proofs and the standard proof theory of
n hyperjumps (e.g., IDn).

I have not seen a reification style proof of EKT. So all of the proofs I
have seen are clearly impredicative under all proposed interpretations of
predicativity.

4. THE LABELED EXTENDED KRUSKAL THEOREM.

LEKT is what I really proved when I proved EKT, and this is the case for all
of the published proofs, as far as I know.

Of course, LEKT immediately implies LKT, and LEKT does not have a
predicative proof, under any proposed interpretation of predicativity.

5. THE GRAPH MINOR THEOREM.

The Graph Minor Theorem of Robertson/Seymour states that a particular qo is
a wqo (finite graphs under minor inclusion), and is proved using all sorts
of constructions of auxiliary qo's relative to given wqo's. This means that
the proof is clearly impredicative on any proposed analysis of
predicativity. 

To clinch the case better, one should identify a particular statement proved
in the course of the proof of GMT that is Pi12 and implies ATR_0. This
should not be difficult to find. I have asked for a memorable item like this
coming up in the course of the proof of GMT, that is not hypertechnical. I
haven't got an answer back yet.

Also I am in extended conversations about what is really needed to prove
GMT. After some discussions with Robertson and Seymour back around the time
of our triple paper,

H. Friedman, N. Robertson, P. Seymour, The Metamathematics of the
Graph Minor Theorem, Logic and Combinatorics, ed. S. Simpson,
AMS Contemporary Mathematics Series, vol. 65, 1987, 229-261.

I was led to believe that GMT is proved within Pi11-CA + BI. However, the
conversations now taking place are going to be more definitive about this. I
will report back when I come to a conclusion.

>From [FRS87] we know that GMT is not provable in Pi11-CA0, and that bounded
GMT is equivalent to Pi11-reflection on Pi11-CA0 over RCA0, and also
equivalent to "theta_Omega_omega(0) is well ordered" over RCA0. Here
"bounded" means "bounded tree width".

6. THE HIGMAN THEOREM.

People often forget that Graham Higman proved what really amounts to labeled
Kruskal's Theorem (bounded valence) EARLIER than Kruskal!

G. Higman, Ordering by divisibility in abstract algebras, Proc. London Math.
Soc. (3), 2:326--336, 1952.

Since this Higman Theorem corresponds to LKT (bounded valence), we know that
it cannot be predicatively proved under any proposed interpretation of
predicativity.

7. THE EFFECTIVE KRUSKAL THEOREM.

I have not explicitly stated these before.

RECURSIVE KT. Let T1,T2,... be a recursive sequence of finite trees. There
exist i < j such that Ti is inf preserving embeddable into Tj.

PRIMITIVE RECURSIVE KT. Let T1,T2,... be a primitive recursive sequence of
finite trees. There exist i < j such that Ti is inf preserving embeddable
into Tj. 

ELEMENTARY RECURSIVE KT. Let T1,T2,... be an elementary recursive sequence
of finite trees. There exist i < j such that Ti is inf preserving embeddable
into Tj. 

THEOREM 7.1. EFA proves the equivalence of Recursive KT with 2-Con(Pi12-BI),
primitive recursive KT with 1-Con(P12-BI), and elementary recursive KT with
1-Con(Pi12-BI).

Here EFA = exponential function arithmetic, 1-Con means "every Sigma01
sentence provable is true", and 2-Con means "every Sigma02 sentence provable
is true".

8. CONCLUSIONS.

Kruskal's theorem comes naturally in Pi11 forms and Pi12 forms. The Pi12
forms involve labels from wqo's.

The Graph Minor Theorem comes naturally in Pi11 form. We are asking about
Pi12 forms, and haven't yet gotten a response.

Higman's Theorem comes naturally in Pi12 form.

All of the Pi11 forms are well beyond Feferman/Schutte predicativity.

All of the Pi12 forms are well beyond any proposed analysis of
predicativity. 

The Pi11 and Pi12 forms are intricately intertwined, and are both extremely
natural. 

*************************************

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 276th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected from
the original.

250. Extreme Cardinals/Pi01  7/31/05  8:34PM
251. Embedding Axioms  8/1/05  10:40AM
252. Pi01 Revisited  10/25/05  10:35PM
253. Pi01 Progress  10/26/05  6:32AM
254. Pi01 Progress/more  11/10/05  4:37AM
255. Controlling Pi01  11/12  5:10PM
256. NAME:finite inclusion theory  11/21/05  2:34AM
257. FIT/more  11/22/05  5:34AM
258. Pi01/Simplification/Restatement  11/27/05  2:12AM
259. Pi01 pointer  11/30/05  10:36AM
260. Pi01/simplification  12/3/05  3:11PM
261. Pi01/nicer  12/5/05  2:26AM
262. Correction/Restatement  12/9/05  10:13AM
263. Pi01/digraphs 1  1/13/06  1:11AM
264. Pi01/digraphs 2  1/27/06  11:34AM
265. Pi01/digraphs 2/more  1/28/06  2:46PM
266. Pi01/digraphs/unifying 2/4/06  5:27AM
267. Pi01/digraphs/progress  2/8/06  2:44AM
268. Finite to Infinite 1  2/22/06  9:01AM
269. Pi01,Pi00/digraphs  2/25/06  3:09AM
270. Finite to Infinite/Restatement  2/25/06  8:25PM
271. Clarification of Smith Article  3/22/06  5:58PM
272. Sigma01/optimal  3/24/06  1:45PM
273: Sigma01/optimal/size  3/28/06  12:57PM
274: Subcubic Graph Numbers  4/1/06  11:23AM
275: Kruskal Theorem/Impredicativity  4/2/06  12:16PM

Harvey Friedman 