of n 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 V 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 v v 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. The set L of all countable linear orderings is well-quasi-ordered under embeddability. 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 minor 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. The set G of all finite graphs is well-quasi-ordered under <=. m One exciting consequence of this theorem is a topological result which 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 M and are minimal with this property. 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 not 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 0 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 h(a,b) = h (b) and consider a the expression h(h(h(0,0),0)+h(0,0),h(0,h(0,0)+h(0,0))) which is a notation for one particular ordinal which is less than G . The 0 above expression may be written in tree form as 0 0 0 0 0 0 h 0 0 0 h h \ / \ / h h 0 + \ / + h h . This is a structured finite tree whose nodes are labeled with the symbols h, +, 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-labeled finite tree to be an ordered pair (T,l) where T is a finite tree and l:T -> {1,2,...,n}. Thus l is a labeling function which assigns to each node x @ T its label l(x) @ {1,2,...,n}. If (T ,l ) and (T ,l ) are two n-labeled 1 1 2 2 finite trees, we say that (T ,l ) is gap-embeddable into (T ,l ) if there 1 1 2 2 exists an embedding f: T ->T with the following additional properties: 1 2 (i) l (x) = l (f(x)) for all x @ T ; (ii) if y @ T is an immediate 1 2 1 1 successor of x @ T , then l (z) >=l (f(y)) for all z @ 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). For each positive integer n, the n-labeled finite trees are well-quasi-ordered under gap-embeddability. 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 quasi-ordinal diagrams 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). For each positive integer n, the set of n-jungles is well-quasi-ordered under embeddability by means of n-jungle morphisms. 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. For each n let S be the set of finite sequences of n elements of {1,2,...,n}. Then S is well-quasi-ordered under gap- n embeddability. " 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 not 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 fin 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 et al. have fin e 0 shown that there is a notion of generalized Goodstein sequence 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 e e 0 The work of Abrusci et al. is based on Girard's notion of dilator which is a category-theoretic approach to ordinal notations. Abrusci et al. 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 hydra game. A hydra 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) Every strategy for Hercules is a winning strategy. (ii) The fact that every recursive strategy for Hercules is a winning strategy cannot be proved in T . fin 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 1 that this fact cannot be proved in the formal system P -CA + BI. By 1 0 considering certain very specific strategies, Buchholz obtains a finite 1 combinatorial theorem which is also not provable in P -CA + BI. 1 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. 1 [6] W. Buchholz, An independence result for (P -CA) + BI, Annals of 1 Pure and Applied Logic, 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, 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 v ' " Mathematics), 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, Proceedings of the American Mathematical Society 87, 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, Advances in Math., 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: Logic Symposium I (Patras 1980), edited by G. Metakides, North-Holland, 1982, pp. 197-220. [16] H. Furstenberg, Recurrence in Ergodic Theory and Combinatorial Number 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 of Symbolic Logic 9, 1944, pp. 33-41. [19] R. L. Graham, B. L. Rothschild, and J. H. Spencer, Ramsey Theory, Wiley, 1980, ix + 174 pages. " [20] A. Kanamori and K. McAloon, On Godel incompleteness and finite combinatorics, 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 for Peano arithmetic, Bulletin of the London Math. Soc. 14, 1982, pp. 285-293. " " [23] D. Konig, Uber eine Schlussweise aus dem Endlichen ins Unendliche, 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 of Math. 93, l971, pp. 89-111. [26] M. Loebl and J. Matousek, On undecidability of the weakened Kruskal theorem, 6 pages, this volume. v v [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, Journal of Symbolic Logic 43, 1978, pp. 725-731. [30] J. Paris and L. Harrington, A mathematical incompleteness in Peano 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: Planar tree-width, Journal of Combinatorial Theory B 36, 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, Archiv " fur math. Logik und Grundlagenforschung 25, 1985, pp. 75-89. " [36] S. G. Simpson, BQO theory and Fraisse's conjecture, Chapter 9 of: 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 combinatorial properties of finite trees, in: Harvey Friedman's Research in the Foundations 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 of the Higman and Kruskal theorems, in: Harvey Friedman's Research in the Foundations 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 Mathematics Pennsylvania State University University Park, PA 16802 Note added September 1, 1986. In a remarkable last-minute ---- ----- --------- -- ---- contribution to this volume, Friedman, Robertson and Seymour have shown that the Robertson-Seymour Theorem 4.6 (well quasiorderedness of finite graphs under minor embeddability) finitistically implies Friedman's Theorem 4.7 (well quasiorderedness of finite labeled trees under gap embeddability). It follows that the Robertson-Seymour Theorem, as well as finite miniaturizations of it, are not provable in the strong system 1 P -CA . Thus the suspicions which were expressed above in connection with 1 0 Theorems 4.6 and 4.7 are fully vindicated.