[FOM] 275:Kruskal Theorem/Impredicativity

Sun Apr 2 12:16:40 EDT 2006

1. Kruskal's theorem.
2. Minimal bad sequences.
3. Labeled Kruskal's theorem.
4. Open questions.

This is a summary of lots of aspects of KT and LKT, which clarifies some
predicativity issues in one place. Everything is pretty much already under
reasonable control in the literature, [1], [2], [3]. However, an old result
of mine cited in section 3, is probably NOT well known, and probably NOT in
the literature (?).

Also see 

[4] S. Simpson, Nonprovability of certain combinatorial properties of finite
trees, 1985, 87-115, in: Harrington, Morley, Scedrov, Simpson (eds.), Harvey
Friedman's Research on the Foundations of Mathematics, Studies in Logic and
the Foundations of Mathematics, North-Holland, 1985.

[5] H. Friedman, Internal finite tree embeddings, Reflections on the
Foundations of Mathematics: Essays in honor of Solomon Feferman, ed. Sieg,
Sommer, Talcott, Lecture Notes in Logic, volume 15, 62-93, 2002, ASL.

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

##############################

1. KRUSKAL'S THEOREM.

Let let us review the situation with the most commonly quoted form of
Kruskal's Theorem.

[1] Joseph B. Kruskal. Well-quasi-ordering, the Tree Theorem, and Vazsonyi's
conjecture. Transactions of the American Mathematical Society , 95:210--225,
May 1960. 

KRUSKAL THEOREM. Let T1,T2,... be finite trees. There exist i < j such that
Ti is inf preserving embeddable into Tj.

There is a well known sharper form of this, also in [1]. A structured tree
is a tree (always in the sense of a poset, not a graph), where the children
of every parent are given a linear ordering.

KRUSKAL THEOREM (with structure). Let T1,T2,... be finite structured trees.
There exist i < j such that Ti is inf and structure preserving embeddable
into Tj.

There is also an important weakening with bounded valence.

KRUSKAL THEROEM (bounded valence). Fix k >= 1. Let T1,T2,... be finite trees
of valence at most k. There exist i < j such that Ti is inf preserving
embeddable into Tj.

KRUSKAL THEOREM (bounded valence, with structure). Fix k >= 1. Let T1,T2,...
be finite structured trees of valence at most k. There exist i < j such that
Ti is inf and structure preserving embeddable into Tj.

THEOREM 1.1. KT, KT (with structure), KT (bounded valence), KT (bounded
valence, with structure), are all provably equivalent to
"theta_capitalomega_0(0) is well ordered" over RCA_0. For each fixed k,
these theorems for valence k are provably equivalent over RCA_0 to the well
ordering of some common specific proper initial segment of
theta_capitalomega_0(0).

COROLLARY 1.2. KT, KT (with structure), KT (bounded valence), KT (bounded
valence, with structure), are all provably equivalent, over RCA_0, to: Pi11
reflection over ACA_0 + Pi12-BI. For each fixed k, these theorems are
provable in ACA_0 + Pi12-BI.

For a treatment of ACA_0 + Pi12-BI see

[2] 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

In light of Theorem 1.2, we say that there is no predicative proof of KT,
under the usual classical interpretation of predicativity by
Feferman/Schutte. 

2. MINIMAL BAD SEQUENCES.

The FIRST, and by far the EASIEST, and most WELL KNOWN proof of KT, is
impredicative on ANY proposed analysis of predicativity. It uses a blatantly
impredicative definition. In fact, the usual proof uses a technique used
throughout this area of combinatorices called

the minimal bad sequence lemma.

MINIMAL BAD SEQUENCE LEMMA. Let Q be a quasi order with domain x1x2,...,
where the x's are distinct. Assume Q is not wqo. Then Q has a minimal bad
sequence. I.e., there exists y1,y2,..., drawn from the x's, such that
1. For no i < j is yi <=Q yj.
2. Suppose z1,z2,..., is a different sequence drawn from the x's, with
property i. There exists i such that yi occurs earlier among the x's, and
for all j < i, yi = zi.

THEOREM 2.1. The minimal bad sequence lemma is provably equivalent to
Pi11-CA0 over RCA0.

See 

[3] A. Marcone, On the logical strength of Nash-William's theorem on
transfinite sequences, 1996, 327-351, in: W. Hodges, M. Hyland, C.
Steinhorn, J. Truss (eds.), Logic: From Foundations to Applications, Keele
1993, Oxford Science Publications, Oxford University Press, 1996.

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. 

We know that we CAN prove Kruskal's theorem WITHOUT resorting to either the
minimal bad sequence lemma AND WITHOUT resorting to any form of labeled
Kruskal's theorem. We know this by PROOF THEORY.

KRUSKAL'S original proof resorts to BOTH the minimal bad sequence lemma AND
labeled Kruskal's theorem.

But I have not seen it done directly. I BELIEVE that it could be done
directly, in an intelligible way, BUT not without additional work, going FAR
BEYOND what J.B. Kruskal did.

We have already seen that if we use the minimal bad sequence lemma, then we
have already done something that is IMPREDICATIVE under any interpretation
of predicativity put forward.

NOW we see what happens with the labeled Kruskal theorem.

3. LABELED KRUSKAL'S THEOREM.

We now discuss the Labeled Kruskal Theorem. It was proved by J.B. Kruskal in
the course of proving the normally quoted Kruskal Theorem.

NOTE: The Labeled Kruskal Theorem is NOT my EKT = Extended Kruskal Theorem.
This is a theorem from J.B. Kruskal, proved as he proved the (ordinary)
Kruskal Theorem. 

In the course of proving KT, Kruskal, in [1], proved a sharper form of KT -
with labels from a wqo.

LABELED KRUSKAL THEOREM. Let T1,T2,... be finite trees with the vertices
labeled from a wqo. There exist i < j such that Ti is inf preserving and
label dominating embeddable into Tj.

LABELED KRUSKAL THEOREM (bounded valence). Fix k >= 1. Let T1,T2,... be
finite trees of valence at most k, with the vertices labeled from a wqo.
There exist i < j such that Ti is inf preserving and label dominating
embeddable into Tj.

THEOREM 3.1. RCA_0 + LKT proves theta_capitalomega_0(1) is well ordered. In
fact, we only need LKT with two discrete labels for this claim.

Thus LKT is stronger than KT, proof theoretically.

THEOREM 3.2. For each fixed k, LKT (bounded valence) is provable in ACA_0 +
Pi12-BI. 

Note that the labeled Kruskal theorem, with or without bounded valence, is a
Pi12 sentence. HOW does it fit into predicativity?

In the 1970's, we proved the following (unpublished).

THEOREM 3.3. Consider the statement "if X is a well ordering then kappa^X is
a well ordering". Here kappa^X is constructed according to Feferman's
original predicative proof theory, where Gamma_0 is the limit of kappa^0,
kappa^kappa^0,... . This statement is provably equivalent to ATR_0 over
RCA_0. 

See, things match nicely in terms of quantifier complexity, since the
statement in quotes is Pi12 and ATR_0 is also Pi12.

THEOREM 3.4. LKT, even for valence 2, implies ATR_0.

So clearly LKT, even for valence 2, is not provable predicatively, under any
interpretation put forward for predicativity.

4. Open Questions.

In [[2], the analysis did not go beyond KT and LKT for bounded valence. And
for LKT, and LKT (bounded valence), there was no provable equivalence with
standard formal systems.  Extend the analysis to KT with various explicit
labels (e.g., finitely many labels, or labels from omega), and to LKT, LKT
(bounded valence). 

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

I use http://www.math.ohio-state.edu/%7Efriedman/ for downloadable
manuscripts. This is the 275th 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

Harvey Friedman