REHMT Kruskal's Theorem is only one highlight of a very interesting branchof combinatorics known as well-quasi-ordering theory (wqo theory forshort). The general notions involved are as follows. A quasi-ordering isa set q (usually infinite) together with a binary relation , which isreflexive and transitive on q. A well-quasi-ordering is a quasi-orderingq with the property that, for every infinite sequence of 8nelements of q, there exist indices i and j such that i < j and Q , Q . @i jThus for example Kruskal's Theorem may be expressed by saying that the sett of all finite trees is wqo under embeddability. There are a number of general theorems which assert that variousmethods of constructing new quasi-orderings from old ones preserve the wqoproperty. For instance, any well-quasi-ordered sum of wqo's is wqo; anyfinite product of wqo's is wqo; the set of finite sequences of elements ofa wqo (appropriately quasi-ordered) is wqo. Some of the deeper results of wqo theory make use of a refined notiondue to Nash-Williams known as better-quasi-ordering (abbreviated bqo).Better-quasi-orderings are more difficult to define and to work with thanwell-quasi-orderings, but they compensate by having better infinitarypreservation properties. For example, the set of transfinite sequences ofelements of a bqo (appropriately quasi-ordered) is bqo. This is not truefor wqo's. A simplified exposition of bqo theory is due to Simpson [36]. For afurther simplification, see the contribution to this volume by vanEngelen, Miller, and Steel [12]. Some recent results of bqo theory are # #discussed in the paper by Nesetril and Thomas [27] in this volume. Thefollowing theorem of Laver [25] is one of the triumphs of bqo theory. 4.5. LAVER'S THEOREM. The set l of all countable linear orderingsis well-quasi-ordered under embeddability. A consequence of Laver's Theorem is that there is no infinite familyof countable linear orderings which are pairwise non-embeddable in eachother. It seems reasonable to speculate that Laver's Theorem and otherresults of bqo theory could give rise to finite combinatorial theoremswhich are unprovable in T or in stronger systems. However, at the finpresent time, there are no solid results in this direction. "* * * One of the most difficult and impressive results of wqo theory is arecent theorem due to Robertson and Seymour. Let G be a finite graph. Aminor of G is any graph which is obtained from G by deleting andcontracting edges. Write H , G if and only if H is isomorphic to a minor mof a subgraph of G. 4.6. ROBERTSON-SEYMOUR THEOREM. The set g of all finite graphs iswell-quasi-ordered under , . m One exciting consequence of this theorem is a topological resultwhich used to be known as Wagner's Conjecture: For any 2-manifold, M,there are only finitely many finite graphs which are not embeddable into Mand are minimal with this property. This generalizes the famous theoremof Kuratowski to the effect that every non-planar graph contains a copy ofeither K or K . 5 3,3 The proof of the Robertson-Seymour Theorem 4.6 is very complicatedand will extend over many journal articles. See for example [33], [34]. In view of Friedman's work as described in #2, it is natural to askwhether the Robertson-Seymour Theorem leads to any finite combinatorialconsequences which are unprovable in T . This is closely tied to &finthe question of which set existence axioms are needed to prove theRobertson-Seymour Theorem. Inspection of the Robertson-Seymour proof shows that it consistslargely of constructive decomposition methods which are formalizable inT . However, Robertson and Seymour also use Kruskal's Theorem in at finleast one crucial point. As explained in #2, Kruskal's Theorem isinherently highly nonconstructive. It is an open question whether theRobertson-Seymour Theorem is equally nonconstructive. For instance, isthe Robertson-Seymour Theorem provable in ATR ? Friedman's work gives us -0reason to suspect that the Robertson-Seymour Theorem is not provable inATR and perhaps not even in some much stronger systems. However, these 0suspicions have not yet been verified. "* * * As explained in #2, Friedman has shown that Kruskal's Theorem and itsfinite form are unprovable in a certain fairly strong subsystem of secondorder arithmetic which is related to the ordinal G . This result is based 20on a direct correlation between finite trees and a notation system for theordinals less than G . 0 To illustrate the correlation, let us write f(a,b) = f (b) and consider ;athe expression f(f(f(0,0),0)+f(0,0),f(0,f(0,0)+f(0,0)))which is a notation for one particular ordinal which is less than G . The C0above expression may be written in tree form as 0 0 0 0 0 0 f 0 0 0 f f \ / \ / f f 0 + '\ / + f \$f .This is a structured finite tree whose nodes are labeled with the symbolsf, +, 0. By means of some coding tricks, one can get rid of the labelsand associate to each ordinal a < G a finite, unlabeled, unstructured #0tree T of the kind considered in Kruskal's Theorem. This can be done in asuch a way that T " T implies a , b. Thus Kruskal's Theorem implies a bthat the ordinals less than G are well-ordered. This close relationship 0between finite trees and ordinal notations is one of the key ideas inFriedman's proof of Theorem 2.3 (exposited in [37]). "* * * In addition, Friedman has found another well-quasi-ordering resultwhich generalizes Kruskal's Theorem and gives rise to certain ordinalnumbers which are much, much larger than G . The generalization is *0phrased in terms of finite trees whose nodes are labeled with positiveintegers. To be precise, if n is a positive integer, we define an n-labeledfinite tree to be an ordered pair (T,l) where T is a finite tree and l:T 3{1,2,...,n}. Thus l is a labeling function which assigns to each node x mT its label l(x) m {1,2,...,n}. If (T ,l ) and (T ,l ) are two n-labeled &1 1 2 2finite trees, we say that (T ,l ) is gap-embeddable into (T ,l ) if there 1 1 2 2exists an embedding f: T 3 T with the following additional properties: 1 2(i) l (x) = l (f(x)) for all x m T ; (ii) if y m T is an immediate 1 2 1 1successor of x m T , then l (z) , l (f(y)) for all z m T in the interval 1 2 2 2f(x) < z < f(y). Friedman's generalization of Kruskal's Theorem reads as follows. 4.7. THEOREM (Friedman). For each positive integer n, the n-labeledfinite trees are well-quasi-ordered under gap-embeddability. This theorem has been used by Robertson and Seymour in their proof ofthe Robertson-Seymour Theorem 4.6. (See [14].) Friedman (unpublished) has shown that Theorem 4.2 and the associatedfinite form (analogous to Theorem 2.2) are not provable in a certain 1well-known formal system P -CA which is much, much stronger than ATR . 1 0 &0In addition, the associated fast-growing functions grow much, much fasterthan f . For an exposition of these results, see Simpson [37]. G 0 "* * * There is a certain obvious definitional resemblance betweenFriedman's n-labeled finite trees and Takeuti's ordinal diagrams of finiteorder [40]. It can also be shown that these two notions give rise to thesame class of ordinal numbers. However, the two notions are conceptuallyquite distinct. For a detailed comparison, see Takeuti [41]. The biggestdifference is that each n-labelled finite tree has only finitely manypredecessors, while ordinal diagrams are well-ordered and typically haveinfinitely many predecessors. In addition, the ordering relation forordinal diagrams is much more difficult to describe than the gap-embeddability relation for finite n-labeled trees. In their contribution to this volume, Okada and Takeuti [28] presenta new notion of quasi-ordinal diagrams which is conceptually intermediatebetween ordinal diagrams and n-labeled finite trees. They show that thenew notion gives rise to even wider classes of ordinal numbers. In this context, it is appropriate to mention another well-quasi-ordering result, due to Klaus Leeb (unpublished). 4.8. THEOREM (Leeb). For each positive integer n, the set ofn-jungles is well-quasi-ordered under embeddability by means of n-junglemorphisms. Unfortunately, the definition of n-jungles and their morphisms iscategory-theoretic and much too complex to be given here. (The definitionwas sketched by Leeb in his talk at this conference and in somehandwritten notes which were circulated after the conference.) It is tempting to conjecture that Leeb's n-jungles give rise to thesame ordinals and fast-growing functions which come out of Friedman'sn-labeled finite trees. However, this conjecture has not yet beenverified. "* * * ~ Schutte and Simpson [35] have considered the problem of what happenswhen Theorem 4.7 (Friedman's generalization of Kruskal's Theorem) isrestricted to the case of finite trees with no ramification, i.e. finitelinearly ordered sets. The resulting combinatorial statement reads asfollows. 4.9. THEOREM. For each n let s be the set of finite sequences of %nelements of {1,2,...,n}. Then s is well-quasi-ordered under gap- nembeddability. ~ Schutte and Simpson [35] show that Theorem 4.9 for each fixed n isprovable in ACA but that the full statement, for all n, is not provable 0in ACA . They also present a Friedman-style finite form of Theorem 4.9 0(analogous to Theorem 2.2) which is not provable in T . This gives yet 5finanother example of a simply stated, "unprovable," finite combinatorialtheorem. "* * * Abrusci, Girard and Van de Wiele [2] have used the Goodstein-Kirby-Paris ideas to obtain finite combinatorial theorems which areunprovable in formal systems which are somewhat stronger than T . ?fin "*Consider for instance the system T which consists of T plus a truth "fin finpredicate for T . The associated ordinal is e . Abrusci et al. have fin e 10shown that there is a notion of generalized Goodstein sequence which isslightly more complicated than Goodstein's and whose convergence to zero *is unprovable in T . The associated growth rate is approximately f . fin 0e Fe G0 The work of Abrusci et al. is based on Girard's notion of dilatorwhich is a category-theoretic approach to ordinal notations. Abrusci etal. have exhibited a general scheme whereby any notation system generatedby dilators gives rise to an associated class of generalized Goodsteinsequences. For an introduction to this work, see the articles by Abrusci[1] and Abrusci, Girard and Van de Wiele [2] in this volume. "* * * The paper of Kirby and Paris [22] on Goodstein sequences containsanother interesting result, concerning the hydra game. A hydra is a finite tree in the sense of #2 above. The hydra game isa certain infinite game with perfect information, taking the form of abattle between Hercules and a given hydra T . For each n , 1, the nth +1move of the game is as follows. First, Hercules chooses a maximal elementy of the finite tree T and deletes it from T , thus forming a new finite n n n - - %-tree T . Then T sprouts n replicas of that part of T which lies above n n %ny 's immediate predecessor, x . The replicas are attached to the n nimmediate predecessor of x . The resulting finite tree is called T . n (n+1 .-(If x is the root of T , then we set T = T .) Hercules wins if and n n n+1 nonly if, for some n, T consists only of its root. n Kirby and Paris have proved the following. 4.10. THEOREM (Kirby-Paris [22]). (i) Every strategy for Herculesis a winning strategy. (ii) The fact that every recursive strategy forHercules is a winning strategy cannot be proved in T . 4fin Thus in 4.10(ii) we have another example of an "unprovable"finitistic theorem. \$* * * The idea of hydra games has been used by Buchholz [6] to give afinite combinatorial theorem which is not provable in a certain formalsystem which is stronger than any that has been mentioned previously inthis paper. The hydras of Buchholz are finite trees whose nodes arelabeled with elements of the set {0,1,2,...,w}. The rules of the Buchholzhydra game are somewhat complicated to describe. Buchholz has shown that,in his hydra game, every strategy for Hercules is a winning strategy, and 61that this fact cannot be proved in the formal system P -CA + BI. By 61 0considering certain very specific strategies, Buchholz obtains a finite 51combinatorial theorem which is also not provable in P -CA + BI. 51 0 For students of proof theory, the Buchholz paper [6] is especiallyto be recommended because of its novel, elegant treatment of cut-elimination for the theories ID , n , w. The Buchholz approach is also nthe basis of the Buchholz-Wainer paper [7] (this volume). The latterpaper provides a streamlined approach to the proof-theoretic ordinals andprovably recursive functions of first order Peano arithmetic. \$* * * No discussion of "unprovable" finite combinatorial theorems would becomplete without mention of the very recent work of Harvey Friedman [13],[14]. Friedman has obtained some striking examples of finite combinatorialtheorems which are "true" but not provable by means of any commonly acceptedmodes of mathematical reasoning. In order to prove these theorems, it isnecessary to use an axiom to the effect that for all n, there exists ann-Mahlo cardinal. Such cardinals extend far beyond the confines of, forinstance, Zermelo-Fraenkel set theory. Recently Ressayre [32] (this volume) has obtained other examplesof finite combinatorial or quasi-combinatorial theorems which areunprovable in, e.g., Zermelo-Fraenkel set theory. Ressayre's methods arebased on model-theoretic results concerning isomorphic initial segmentsof models of set theory. References. __________ [1] V. M. Abrusci, Dilators, generalized Goodstein sequences,independence results: a survey, 20 pages, this volume. [2] V. M. Abrusci, J.-Y. Girard, and J. Van de Wiele, Some uses ofdilators in combinatorial problems I, 27 pages, this volume. [3] V. Bergelson, Ergodic Ramsey theory, 26 pages, this volume. [4] A. Blass, J. L. Hirst, and S. G. Simpson, Logical analysis ofsome theorems of combinatorics and topological dynamics, 32 pages, thisvolume. [5] S. Brackin, A summary of "On Ramsey-type theorems and theirprovability in weak formal systems", 10 pages, this volume. 31 [6] W. Buchholz, An independence result for (P -CA) + BI, Annals of 31Pure and Applied Logic, to appear. [7] W. Buchholz and S. Wainer, Provably computable funcions and thefast-growing hierarchy, 20 pages, this volume. [8] T. J. Carlson and S. G. Simpson, A dual form of Ramsey's Theorem,Advances in Mathematics 53, 1984, pp. 265-290. [9] T. J. Carlson and S. G. Simpson, Topological Ramsey Theory, in:Mathematics of Ramsey Theory (a special volume of Annals of Discrete # ' ~Mathematics), edited by J. Nesetril and V. Rodl, to appear. [10] E. A. Cichon, A short proof of two recently discoveredindependence results using recursion theoretic methods, Proceedings ofthe American Mathematical Society 87, 1983, pp. 704-706. [12] F. van Engelen, A. W. Miller, and J. Steel, Rigid Borel sets andbetter quasiorder theory, 27 pages, this volume. [13] H. Friedman, Necessary uses of abstract set theory in finitemathematics, Advances in Math., to appear. [14] H. Friedman, Update on concrete independence, February l986, 6pages. [15] H. Friedman, K. McAloon, and S. G. Simpson, A finitecombinatorial principle which is equivalent to the 1-consistency ofpredicative analysis, in: Logic Symposium I (Patras 1980), edited by G.Metakides, North-Holland, 1982, pp. 197-220. [16] H. Furstenberg, Recurrence in Ergodic Theory and CombinatorialNumber Theory, Princeton University Press, 1981, vii + 202 pages. [17] F. Galvin and K. Prikry, Borel sets and Ramsey's Theorem,Journal of Symbolic Logic 38, 1973, pp. 193-198. [18] R. L. Goodstein, On the restricted ordinal theorem, Journal ofSymbolic Logic 9, 1944, pp. 33-41. [19] R. L. Graham, B. L. Rothschild, and J. H. Spencer, RamseyTheory, Wiley, 1980, ix + 174 pages. *~ [20] A. Kanamori and K. McAloon, On Godel incompleteness and finitecombinatorics, Annals of Pure and Applied Logic, to appear. [21] J. Ketonen and R. Solovay, Rapidly growing Ramsey functions,Annals of Mathematics 113, 1981, pp. 267-314. [22] L. Kirby and J. Paris, Accessible independence results forPeano arithmetic, Bulletin of the London Math. Soc. 14, 1982, pp.285-293. ~ ~ [23] D. Konig, Uber eine Schlussweise aus dem Endlichen insUnendliche, Acta Litterarum ac Scientarum (Ser. Sci. Math.) Szeged 3,1927, pp. 121-130. [24] J. Kruskal, Well-quasi-ordering, the tree theorem, and 'Vazsonyi's conjecture, Transactions of the Amer. Math. Soc. 95, 1960, pp.210-225. ~ [25] R. Laver, On Fraisse's order type conjecture, Annals ofMath. 93, l971, pp. 89-111. [26] M. Loebl and J. Matousek, On undecidability of the weakenedKruskal theorem, 6 pages, this volume. # # [27] J. Nesetril and R. Thomas, Well quasiorderings, long games, anda combinatorial study of undecidability, 13 pages, this volume. [28] M. Okada and G. Takeuti, On the theory of quasi ordinaldiagrams, 14 pages, this volume. [29] J. Paris, Some independence results for Peano arithmetic,Journal of Symbolic Logic 43, 1978, pp. 725-731. [30] J. Paris and L. Harrington, A mathematical incompleteness inPeano arithmetic, in: Handbook of Mathematical Logic, edited by J.Barwise, North-Holland, 1977, pp. 1133-1142. [31] F. P. Ramsey, On a problem of formal logic, Proc. London Math.Soc. 30, 1930, pp. 264-286. [32] J.-P. Ressayre, Nonstandard universes with strong embeddings,and their finite approximations, 20 pages, this volume. [33] N. Robertson and P. D. Seymour, Graph minors III: Planartree-width, Journal of Combinatorial Theory B 36, 1984, pp. 49-64. [34] N. Robertson and P. D. Seymour, Graph minors VII: a Kuratowskitheorem for general surfaces, preprint, 38 pages. ~ [35] K. Schutte and S. G. Simpson, Ein in der reinen Zahlentheorie ~ ~unbeweisbarer Satz uber endliche folgen von naturlichen Zahlen, Archiv ~fur math. Logik und Grundlagenforschung 25, 1985, pp. 75-89. +~ [36] S. G. Simpson, BQO theory and Fraisse's conjecture, Chapter 9of: Recursive Aspects of Descriptive Set Theory, by R. Mansfield and G.Weitkamp, Oxford University Press, 1985, pp. 124-138. [37] S. G. Simpson, Nonprovability of certain combinatorialproperties of finite trees, in: Harvey Friedman's Research in theFoundations of Mathematics, edited by L. Harrington, M. Morley, A.Scedrov, and S. G. Simpson, North-Holland, l985, pp. 87-117. [38] S. G. Simpson, Partial realizations of Hilbert's Program,preprint, 1986, 21 pages. [39] R. L. Smith, The consistency strength of some finite forms ofthe Higman and Kruskal theorems, in: Harvey Friedman's Research in theFoundations of Mathematics, edited by L. Harrington, M. Morley, A.Scedrov, and S. G. Simpson, North-Holland, l985, pp. 87-117. [40] G. Takeuti, Ordinal diagrams, J. Math. Soc. Japan 9, 1957, pp.386-394; 12, 1960, pp. 385-391. [41] G. Takeuti, Proof Theory (second edition), North-Holland, 1986,to appear.Department of MathematicsPennsylvania State UniversityUniversity Park, PA 16802