of 8nelements of q, there exist indices i and j such that i < j and Q , Q . @i jThus for example Kruskal's Theorem may be expressed by saying that the sett of all finite trees is wqo under embeddability. There are a number of general theorems which assert that variousmethods of constructing new quasi-orderings from old ones preserve the wqoproperty. For instance, any well-quasi-ordered sum of wqo's is wqo; anyfinite product of wqo's is wqo; the set of finite sequences of elements ofa wqo (appropriately quasi-ordered) is wqo. Some of the deeper results of wqo theory make use of a refined notiondue to Nash-Williams known as better-quasi-ordering (abbreviated bqo).Better-quasi-orderings are more difficult to define and to work with thanwell-quasi-orderings, but they compensate by having better infinitarypreservation properties. For example, the set of transfinite sequences ofelements of a bqo (appropriately quasi-ordered) is bqo. This is not truefor wqo's. A simplified exposition of bqo theory is due to Simpson [36]. For afurther simplification, see the contribution to this volume by vanEngelen, Miller, and Steel [12]. Some recent results of bqo theory are # #discussed in the paper by Nesetril and Thomas [27] in this volume. Thefollowing theorem of Laver [25] is one of the triumphs of bqo theory. 4.5. LAVER'S THEOREM. The set l of all countable linear orderingsis well-quasi-ordered under embeddability. A consequence of Laver's Theorem is that there is no infinite familyof countable linear orderings which are pairwise non-embeddable in eachother. It seems reasonable to speculate that Laver's Theorem and otherresults of bqo theory could give rise to finite combinatorial theoremswhich are unprovable in T or in stronger systems. However, at the finpresent time, there are no solid results in this direction. "* * * One of the most difficult and impressive results of wqo theory is arecent theorem due to Robertson and Seymour. Let G be a finite graph. Aminor of G is any graph which is obtained from G by deleting andcontracting edges. Write H , G if and only if H is isomorphic to a minor mof a subgraph of G. 4.6. ROBERTSON-SEYMOUR THEOREM. The set g of all finite graphs iswell-quasi-ordered under , . m One exciting consequence of this theorem is a topological resultwhich used to be known as Wagner's Conjecture: For any 2-manifold, M,there are only finitely many finite graphs which are not embeddable into Mand are minimal with this property. This generalizes the famous theoremof Kuratowski to the effect that every non-planar graph contains a copy ofeither K or K . 5 3,3 The proof of the Robertson-Seymour Theorem 4.6 is very complicatedand 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 askwhether the Robertson-Seymour Theorem leads to any finite combinatorialconsequences which are unprovable in T . This is closely tied to &finthe question of which set existence axioms are needed to prove theRobertson-Seymour Theorem. Inspection of the Robertson-Seymour proof shows that it consistslargely of constructive decomposition methods which are formalizable inT . However, Robertson and Seymour also use Kruskal's Theorem in at finleast one crucial point. As explained in #2, Kruskal's Theorem isinherently highly nonconstructive. It is an open question whether theRobertson-Seymour Theorem is equally nonconstructive. For instance, isthe Robertson-Seymour Theorem provable in ATR ? Friedman's work gives us -0reason to suspect that the Robertson-Seymour Theorem is not provable inATR and perhaps not even in some much stronger systems. However, these 0suspicions have not yet been verified. "* * * As explained in #2, Friedman has shown that Kruskal's Theorem and itsfinite form are unprovable in a certain fairly strong subsystem of secondorder arithmetic which is related to the ordinal G . This result is based 20on a direct correlation between finite trees and a notation system for theordinals less than G . 0 To illustrate the correlation, let us write f(a,b) = f (b) and consider ;athe 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 C0above 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 symbolsf, +, 0. By means of some coding tricks, one can get rid of the labelsand associate to each ordinal a < G a finite, unlabeled, unstructured #0tree T of the kind considered in Kruskal's Theorem. This can be done in asuch a way that T " T implies a , b. Thus Kruskal's Theorem implies a bthat the ordinals less than G are well-ordered. This close relationship 0between finite trees and ordinal notations is one of the key ideas inFriedman's proof of Theorem 2.3 (exposited in [37]). "* * * In addition, Friedman has found another well-quasi-ordering resultwhich generalizes Kruskal's Theorem and gives rise to certain ordinalnumbers which are much, much larger than G . The generalization is *0phrased in terms of finite trees whose nodes are labeled with positiveintegers. To be precise, if n is a positive integer, we define an n-labeledfinite tree 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 mT its label l(x) m {1,2,...,n}. If (T ,l ) and (T ,l ) are two n-labeled &1 1 2 2finite trees, we say that (T ,l ) is gap-embeddable into (T ,l ) if there 1 1 2 2exists 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 1successor of x m T , then l (z) , l (f(y)) for all z m T in the interval 1 2 2 2f(x) < z < f(y). Friedman's generalization of Kruskal's Theorem reads as follows. 4.7. THEOREM (Friedman). For each positive integer n, the n-labeledfinite trees are well-quasi-ordered under gap-embeddability. This theorem has been used by Robertson and Seymour in their proof ofthe Robertson-Seymour Theorem 4.6. (See [14].) Friedman (unpublished) has shown that Theorem 4.2 and the associatedfinite form (analogous to Theorem 2.2) are not provable in a certain 1well-known formal system P -CA which is much, much stronger than ATR . 1 0 &0In addition, the associated fast-growing functions grow much, much fasterthan f . For an exposition of these results, see Simpson [37]. G 0 "* * * There is a certain obvious definitional resemblance betweenFriedman's n-labeled finite trees and Takeuti's ordinal diagrams of finiteorder [40]. It can also be shown that these two notions give rise to thesame class of ordinal numbers. However, the two notions are conceptuallyquite distinct. For a detailed comparison, see Takeuti [41]. The biggestdifference is that each n-labelled finite tree has only finitely manypredecessors, while ordinal diagrams are well-ordered and typically haveinfinitely many predecessors. In addition, the ordering relation forordinal 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] presenta new notion of quasi-ordinal diagrams which is conceptually intermediatebetween ordinal diagrams and n-labeled finite trees. They show that thenew 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). For each positive integer n, the set ofn-jungles is well-quasi-ordered under embeddability by means of n-junglemorphisms. Unfortunately, the definition of n-jungles and their morphisms iscategory-theoretic and much too complex to be given here. (The definitionwas sketched by Leeb in his talk at this conference and in somehandwritten notes which were circulated after the conference.) It is tempting to conjecture that Leeb's n-jungles give rise to thesame ordinals and fast-growing functions which come out of Friedman'sn-labeled finite trees. However, this conjecture has not yet beenverified. "* * * ~ Schutte and Simpson [35] have considered the problem of what happenswhen Theorem 4.7 (Friedman's generalization of Kruskal's Theorem) isrestricted to the case of finite trees with no ramification, i.e. finitelinearly ordered sets. The resulting combinatorial statement reads asfollows. 4.9. THEOREM. For each n let s be the set of finite sequences of %nelements of {1,2,...,n}. Then s is well-quasi-ordered under gap- nembeddability. ~ Schutte and Simpson [35] show that Theorem 4.9 for each fixed n isprovable in ACA but that the full statement, for all n, is not provable 0in 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 5finanother example of a simply stated, "unprovable," finite combinatorialtheorem. "* * * Abrusci, Girard and Van de Wiele [2] have used the Goodstein-Kirby-Paris ideas to obtain finite combinatorial theorems which areunprovable in formal systems which are somewhat stronger than T . ?fin "*Consider for instance the system T which consists of T plus a truth "fin finpredicate for T . The associated ordinal is e . Abrusci et al. have fin e 10shown that there is a notion of generalized Goodstein sequence which isslightly more complicated than Goodstein's and whose convergence to zero *is unprovable in T . The associated growth rate is approximately f . fin 0e Fe G0 The work of Abrusci et al. is based on Girard's notion of dilatorwhich is a category-theoretic approach to ordinal notations. Abrusci etal. have exhibited a general scheme whereby any notation system generatedby dilators gives rise to an associated class of generalized Goodsteinsequences. 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 containsanother interesting result, concerning the hydra game. A hydra is a finite tree in the sense of #2 above. The hydra game isa certain infinite game with perfect information, taking the form of abattle between Hercules and a given hydra T . For each n , 1, the nth +1move of the game is as follows. First, Hercules chooses a maximal elementy 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 %ny 's immediate predecessor, x . The replicas are attached to the n nimmediate 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 nonly 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) Every strategy for Herculesis a winning strategy. (ii) The fact that every recursive strategy forHercules is a winning strategy cannot be proved in 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 afinite combinatorial theorem which is not provable in a certain formalsystem which is stronger than any that has been mentioned previously inthis paper. The hydras of Buchholz are finite trees whose nodes arelabeled with elements of the set {0,1,2,...,w}. The rules of the Buchholzhydra game are somewhat complicated to describe. Buchholz has shown that,in his hydra game, every strategy for Hercules is a winning strategy, and 61that this fact cannot be proved in the formal system P -CA + BI. By 61 0considering certain very specific strategies, Buchholz obtains a finite 51combinatorial theorem which is also not provable in P -CA + BI. 51 0 For students of proof theory, the Buchholz paper [6] is especiallyto be recommended because of its novel, elegant treatment of cut-elimination for the theories ID , n , w. The Buchholz approach is also nthe basis of the Buchholz-Wainer paper [7] (this volume). The latterpaper provides a streamlined approach to the proof-theoretic ordinals andprovably recursive functions of first order Peano arithmetic. $* * * No discussion of "unprovable" finite combinatorial theorems would becomplete without mention of the very recent work of Harvey Friedman [13],[14]. Friedman has obtained some striking examples of finite combinatorialtheorems which are "true" but not provable by means of any commonly acceptedmodes of mathematical reasoning. In order to prove these theorems, it isnecessary to use an axiom to the effect that for all n, there exists ann-Mahlo cardinal. Such cardinals extend far beyond the confines of, forinstance, Zermelo-Fraenkel set theory. Recently Ressayre [32] (this volume) has obtained other examplesof finite combinatorial or quasi-combinatorial theorems which areunprovable in, e.g., Zermelo-Fraenkel set theory. Ressayre's methods arebased on model-theoretic results concerning isomorphic initial segmentsof 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 ofdilators 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 ofsome theorems of combinatorics and topological dynamics, 32 pages, thisvolume. [5] S. Brackin, A summary of "On Ramsey-type theorems and theirprovability in weak formal systems", 10 pages, this volume. 31 [6] W. Buchholz, An independence result for (P -CA) + BI, Annals of 31Pure and Applied Logic, to appear. [7] W. Buchholz and S. Wainer, Provably computable funcions and thefast-growing hierarchy, 20 pages, this volume. [8] T. J. Carlson and S. G. Simpson, A dual form of Ramsey's Theorem,Advances in Mathematics 53, 1984, pp. 265-290. [9] T. J. Carlson and S. G. Simpson, Topological Ramsey Theory, in:Mathematics of Ramsey Theory (a special volume of Annals of Discrete # ' ~Mathematics), edited by J. Nesetril and V. Rodl, to appear. [10] E. A. Cichon, A short proof of two recently discoveredindependence results using recursion theoretic methods, Proceedings ofthe American Mathematical Society 87, 1983, pp. 704-706. [12] F. van Engelen, A. W. Miller, and J. Steel, Rigid Borel sets andbetter quasiorder theory, 27 pages, this volume. [13] H. Friedman, Necessary uses of abstract set theory in finitemathematics, Advances in Math., to appear. [14] H. Friedman, Update on concrete independence, February l986, 6pages. [15] H. Friedman, K. McAloon, and S. G. Simpson, A finitecombinatorial principle which is equivalent to the 1-consistency ofpredicative analysis, in: Logic Symposium I (Patras 1980), edited by G.Metakides, North-Holland, 1982, pp. 197-220. [16] H. Furstenberg, Recurrence in Ergodic Theory and CombinatorialNumber Theory, Princeton University Press, 1981, vii + 202 pages. [17] F. Galvin and K. Prikry, Borel sets and Ramsey's Theorem,Journal of Symbolic Logic 38, 1973, pp. 193-198. [18] R. L. Goodstein, On the restricted ordinal theorem, Journal ofSymbolic Logic 9, 1944, pp. 33-41. [19] R. L. Graham, B. L. Rothschild, and J. H. Spencer, RamseyTheory, Wiley, 1980, ix + 174 pages. *~ [20] A. Kanamori and K. McAloon, On Godel incompleteness and finitecombinatorics, Annals of Pure and Applied Logic, to appear. [21] J. Ketonen and R. Solovay, Rapidly growing Ramsey functions,Annals of Mathematics 113, 1981, pp. 267-314. [22] L. Kirby and J. Paris, Accessible independence results forPeano arithmetic, Bulletin of the London Math. Soc. 14, 1982, pp.285-293. ~ ~ [23] D. Konig, Uber eine Schlussweise aus dem Endlichen insUnendliche, Acta Litterarum ac Scientarum (Ser. Sci. Math.) Szeged 3,1927, pp. 121-130. [24] J. Kruskal, Well-quasi-ordering, the tree theorem, and 'Vazsonyi's conjecture, Transactions of the Amer. Math. Soc. 95, 1960, pp.210-225. ~ [25] R. Laver, On Fraisse's order type conjecture, Annals ofMath. 93, l971, pp. 89-111. [26] M. Loebl and J. Matousek, On undecidability of the weakenedKruskal theorem, 6 pages, this volume. # # [27] J. Nesetril and R. Thomas, Well quasiorderings, long games, anda combinatorial study of undecidability, 13 pages, this volume. [28] M. Okada and G. Takeuti, On the theory of quasi ordinaldiagrams, 14 pages, this volume. [29] J. Paris, Some independence results for Peano arithmetic,Journal of Symbolic Logic 43, 1978, pp. 725-731. [30] J. Paris and L. Harrington, A mathematical incompleteness inPeano arithmetic, in: Handbook of Mathematical Logic, edited by J.Barwise, North-Holland, 1977, pp. 1133-1142. [31] F. P. Ramsey, On a problem of formal logic, Proc. London Math.Soc. 30, 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: Planartree-width, Journal of Combinatorial Theory B 36, 1984, pp. 49-64. [34] N. Robertson and P. D. Seymour, Graph minors VII: a Kuratowskitheorem 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, Archiv ~fur math. Logik und Grundlagenforschung 25, 1985, pp. 75-89. +~ [36] S. G. Simpson, BQO theory and Fraisse's conjecture, Chapter 9of: Recursive Aspects of Descriptive Set Theory, by R. Mansfield and G.Weitkamp, Oxford University Press, 1985, pp. 124-138. [37] S. G. Simpson, Nonprovability of certain combinatorialproperties of finite trees, in: Harvey Friedman's Research in theFoundations of Mathematics, 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 ofthe Higman and Kruskal theorems, in: Harvey Friedman's Research in theFoundations of Mathematics, edited by L. Harrington, M. Morley, A.Scedrov, and S. G. Simpson, North-Holland, l985, pp. 87-117. [40] G. Takeuti, Ordinal diagrams, J. Math. Soc. Japan 9, 1957, pp.386-394; 12, 1960, pp. 385-391. [41] G. Takeuti, Proof Theory (second edition), North-Holland, 1986,to appear.Department of MathematicsPennsylvania State UniversityUniversity Park, PA 16802