p...@mtnmath.com (Paul Budnik) wrote to sci.math,sci.physics on 5/27/96:
:
: Of course you can change the name of `truth' or anything else.
: So what. What is central to mathematics is that certain propositions
: are deducible from certain formal systems. Without that formal
: mathematics is impossible. With it you have the objective truth
: of at least finite mathematics. ...
:
: There is general agreement that objective mathematical truth exists.
: The vast majority of mathematicians will agree
: on at least the objective truth of finite mathematics.
But there is no such thing as a comprehensive, self-contained discipline
of finite mathematics. Any such system suffers suffers from Goedel
incompleteness, and there are by now well-known "natural" independence
results which serve to show that such incompleteness results are not
just contrived uninteresting curiosities. There is simply no way of
avoiding infinity when it comes to truth.
Perhaps the best exposition along these lines is Steven Simpson's
paper "Unprovable theorems and fast-growing functions", Contemporary
Math. 65 1987, 359-394. I've appended an asciized version of this
paper below (the original is at ftp.math.psu.edu:/pub/simpson).
See also my earlier sci.math posts on Goedel incompleteness,
Goodstein's Theorem, Kruskal's Theorem, etc. which you may find via
the newsgroup archives at http://www.dejanews.com/.
-Bill
UNPROVABLE THEOREMS AND FAST-GROWING FUNCTIONS
Contemporary Math. 65 1987, 359-394
Stephen G. Simpson
#0. Introduction.
------------
This paper is a write-up of an expository talk which I have given to
mathematical audiences at a number of universities in the United States
and Europe over a period of several years. Preparation of this paper was
partially supported by NSF grant DMS-8317874.
The purpose of the talk is to exposit some recent results (1977 and
later) in which mathematical logic has impinged upon finite combinatorics.
Like most good research in mathematical logic, the results which I am
going to discuss had their origin in philosophical problems concerning the
foundations of mathematics. Specifically, the results discussed here were
inspired by the following philosophical question. Could there be such a
thing as a comprehensive, self-contained discipline of finite
combinatorial mathematics?
It is well known that a great deal of reasoning about finite
combinatorial structures can be carried out in a self-contained finitary
way, i.e. with no reference whatsoever to infinite sets or structures. I
have in mind whole branches of mathematics such as finite graph theory,
finite lattice theory, finite geometries, block designs, large parts of
finite group theory (excluding character theory, in which use is made of
the field of complex numbers), and large parts of number theory (including
the elementary parts but excluding analytical techniques such as contour
integrals). One could easily imagine comprehensive textbooks of these
subjects in which infinite sets are never mentioned, even tangentially.
All of the reasoning in such textbooks would be concerned exclusively with
finite sets and structures.
Consequently, there is a strong naive impression that the answer to
our above-mentioned philosophical question is "yes."
However, naive impressions can be misleading. I am going to discuss
three recent results from mathematical logic which point to an answer of
"no." Namely, I shall present three examples of combinatorial theorems
which are finitistic in their statements but not in their proofs. Each of
the three theorems is simple and elegant and refers only to finite
structures. Each of the three theorems has a simple and elegant proof.
The only trouble is that each of the proofs uses an infinite set at some
crucial point. Moreover, deep logical investigations have shown that the
infinite sets are in fact indispensable. Any proof of one of these finite
combinatorial theorems must involve a detour through the infinite. Thus,
in a strong relative sense, the three theorems are "unprovable" -- they
cannot be proved by means of the finite combinatorial considerations in
terms of which they are stated.
There is one somewhat technical point from mathematical logic which I
must now discuss. This involves the answer to a question which may have
already occurred to the reader. Namely, how might one establish that a
given finite combinatorial theorem cannot be given a finite combinatorial
proof? We know how to recognize a finite combinatorial proof when we see
one. But how could we hope to establish that there is no finite
combinatorial proof of a given theorem? In order to do this, it would be
first of all necessary to give a precise definition of "finite
combinatorial proof" or at least "finite combinatorial provability."
Such a definition has in fact been formulated and validated by
mathematical logicians. The definition is unquestionably adequate in that
it is precise, rigorous, and captures the intuitive idea of "provability
by finite combinatorial means." I do not want to give the detailed
definition here. I shall however say something about the definition.
(The details can be found in any good first-year graduate course or
textbook on the foundations of mathematics. For readers who are trained
in mathematical logic, let me remark that the notion I have in mind is
that of provability in the formal system PA of first-order Peano
arithmetic, also known as Z . Equivalently, one could consider
1
provability in the formal system consisting of Zermelo-Fraenkel set theory
with the axiom of infinity replaced by "All sets are finite.")
More specifically, there is a formal system consisting of appropriate
symbols, formulas, axioms, and rules of inference. For my purposes here I
shall refer to this formal system as T , the theory of finite sets and
fin
structures. The language of T contains variables which can denote
fin
arbitrary finite sets or finite structures of various sorts. For
instance, there could be variables ranging over natural numbers, finite
sequences of natural numbers, finite unordered sets, finite ordered sets,
finite sequences of finite unordered sets, etc. Quantification over such
finite structures is permitted. For instance, we can write down a formula
saying that for any finite structure of a certain sort there exists
another finite structure bearing a certain relationship to the first one,
etc. There are also logical connectives which have their usual meaning.
All valid methods of finite combinatorial inference are either formulated
explicitly as rules of the formal system T or can be derived from rules
fin
which are are so formulated. For instance, T includes the powerful
fin
principle of proof by induction on the cardinality of a finite
combinatorial structure of a given sort. This principle applies to any
property of finite structures which can be expressed by a formula of the
language of T .
fin
The point of T is that our intuitive but imprecise concept of
fin
"finite combinatorial provability" can be replaced by the precisely
defined notion of "provability in the formal system T ." This makes it
fin
possible for logicians to state and prove results to the effect that
particular finite combinatorial theorems cannot be given finite
combinatorial proofs.
The body of this paper is devoted to a fairly detailed discussion of
the above-mentioned three examples of "unprovable" theorems. The three
theorems involve respectively colorings of finite sets, embeddings of
finite trees, and exponential notation. I shall discuss the three
examples one at a time together with appropriate background material. In
each case I shall present the finite combinatorial theorem and at least a
sketch of its proof. I shall then give indications of why the theorem
cannot be proved in T , i.e. why any proof must involve a detour through
fin
the infinite. This will require some discussion of ordinal numbers and of
a hierarchy of fast-growing functions.
At the end of the paper there is an appendix describing subsequent,
related research. (The material in the appendix was not included in the
talk on which this paper is based.) For further details I refer to the
literature, including several of the other papers in this volume.
#1. A variant of Ramsey's Theorem.
- ------- -- -------- -------
Our first example of an "unprovable" theorem of finite combinatorics
concerns colorings of the k-element subsets of a given finite set. It is
closely related to a famous theorem of Ramsey [31]. I begin by recalling
the Finite Ramsey Theorem.
If X is any finite set, we write |X| = cardinality of X. We use i,
j, k, l, m and n to denote positive integers. If X is any set, we
k
denote by [X] the set of all k-element subsets of X.
1.1. FINITE RAMSEY THEOREM (Ramsey [31]). For all k, l and m,
k
there exists n so large that: if |X| = n and [X] = C U ... U C ,
1 l
k
then there exists Y <=X such that |Y| >=m and [Y] <=C for some i
i
<=l.
The reader who has no previous acquaintance with Ramsey's Theorem may
find the following sociological illustration useful. Suppose that k = l =
2. In this case the Finite Ramsey Theorem says the following. For any m,
there exists n so large that, in any gathering of n people, there will
always be a set of at least m of them who all know each other, or none of
whom know each other. Here C (respectively C ) is the set of unordered
1 2
pairs of people who know each other (respectively do not know each other).
For example, if m = 3 then we may take n = 6. This means that in any
gathering of 6 people, there will always be at least three who either all
know each other or all don't know each other.
In the statement of the Finite Ramsey Theorem, there is no harm in
assuming that the sets C , ..., C are pairwise disjoint. In this case,
1 l
k
the hypothesis [X] = C U ... U C is sometimes expressed by saying
1 l
that the k-element subsets of X have been colored with l colors C , ...,
1
C .
l
The Finite Ramsey Theorem is definitely not our promised example of
an "unprovable" theorem. Like the vast majority of finite combinatorial
theorems, the Finite Ramsey Theorem has a finitistic proof which is
straightforwardly formalizable in T . I shall not give the proof here,
fin
but in order to give the reader a feeling for this, let me mention that
the proof yields an easily described upper bound on the size of n
(expressed as a function of the other parameters k, l, and m). Let us
denote by f (k,l,m) the smallest n such that the conclusion of the
R
Finite Ramsey Theorem holds. The function f is known in the literature
R
as "the Ramsey function." One of the standard proofs of the Finite Ramsey
Theorem (namely the proof by "ramification") yields an upper bound of
approximately
m+2k
l \
. |
. > k+1
. |
l |
l /
for f (k,l,m). It is also known that f (k,l,m) is bounded below by a
R R
similar expression. Thus f (k,l,m) is of superexponential growth rate
R
in the parameter k. Such growth rates fall well within the strictures of
finite combinatorial provability.
We shall now state a finite combinatorial theorem which looks very
similar to the Finite Ramsey Theorem and may appear to be only slightly
stronger. However, we shall see that the logical properties and growth
rates which are associated to this Modified Finite Ramsey Theorem are
strikingly different from those of the original Finite Ramsey Theorem.
1.2. MODIFIED FINITE RAMSEY THEOREM. For all k, l and m there
k
exists n so large that: if X = {1,2,...,n} and if [X] = C U ...
1
U C , then there exists Y <=X such that |Y| >=m, |Y| >=min(Y), and
l
k
[Y] <=C for some i <=l.
i
The Modified Finite Ramsey Theorem can be restated as follows. A
finite nonempty set Y of positive integers is said to be relatively
large if |Y| >=min(Y), i.e. the cardinality of Y is at least as great
as the minimum element of Y. For example {3,6,7} is relatively large and
{6,7,9,11,15} is not relatively large. The Modified Finite Ramsey Theorem
is just the Finite Ramsey Theorem with the conclusion strengthened to say
that in addition Y is relatively large. This is a transparent
generalization of the Finite Ramsey Theorem.
Consider for instance the sociological illustration which was
discussed earlier. In those terms, the special case k = l = 2 of the
Modified Finite Ramsey Theorem says the following. Given m, there exists
n so large that the following holds. Consider an arbitrary set of n
th
people with the property that, for each j <=n, the j person in the set
is of the opinion that the number j is a very big number. Then there
will have to be a subset consisting of at least m people all of whom
know each other or all of whom do not know each other, such that in
addition the subset is very big according to the opinion of at least one
of the people in the subset.
We now come to the main point of this section. The Modified Finite
Ramsey Theorem was first formulated by Paris and Harrington in order to
enable them to state the following unprovability result.
1.3. THEOREM (Paris-Harrington [30]). The Modified Finite Ramsey
Theorem is not provable in T . In other words, the Modified Finite
fin
Ramsey Theorem cannot be proved by finite combinatorial means alone.
Thus the Modified Finite Ramsey Theorem is our first example of an
"unprovable" combinatorial theorem. As explained above, the unprovability
is only relative. The Modified Finite Ramsey Theorem is a valid
mathematical theorem which is proved by standard combinatorial methods.
The only unusual feature is that, although the statement of the theorem is
strictly finitistic, any proof of the theorem must necessarily involve the
infinite.
For interest's sake I shall now give the proof of the Modified Finite
Ramsey Theorem. The proof is simple but uses infinite sets. It is based
on the following well-known infinitistic version of Ramsey's Theorem.
1.4. INFINITE RAMSEY THEOREM (Ramsey [31]). Let X be an infinite
k
set. If [X] = C U ... U C , then there exists an infinite set Y <=
1 l
k
X such that [Y] <= C for some i <=l.
i
I shall deduce the Modified Finite Ramsey Theorem from the Infinite
Ramsey Theorem. Suppose that the Modified Finite Ramsey Theorem is false.
Then for some fixed k, l, and m, there is no n satisfying the
conclusion of the theorem. In other words, for each n there is a
k n n
coloring [{1,...,n}] = C U ... U C such that for no Y <={1,...,n}
1 l
k n
and i <=l do we have |Y| >=m, |Y| >=min(Y), [Y] <=C . Let X be the
i
set of all positive integers. For each i <=l let C be the set of all
i
n
(k+1)-element subsets of X of the form F U {n+1} with F @ C . Thus
i
k+1
[X] = C U ... U C and there is no finite Y <=X such that |Y| >=m
1 l
k+1
+ 1, |Y| >=min(Y) + 1, [Y] <=C for some i <=l. Hence there is no
i
k+1
infinite Y <=X such that [Y] <=C for some i <=l. This is in
i
contradiction to the Infinite Ramsey Theorem.
As indicated above, Paris and Harrington have shown that the Modified
Finite Ramsey Theorem cannot be given a finite combinatorial proof. In
order to give some indication of why this is so, we shall now discuss the
associated fast-growing function. Given k, l, and m, let f (k,l,m) be
PH
the smallest n which satisfies the conclusion of the Modified Finite
Ramsey Theorem. Recall that f (k,l,m) is the analogous function for the
R
original Finite Ramsey Theorem. One way to highlight the difference
between the Finite Ramsey Theorem and the Modified Finite Ramsey Theorem
is to compare the growth rates of f and f . We shall see that f grows
R PH PH
much faster than f .
R
We have already described the growth rate of f . In order to
R
describe the growth rate of f , it will be necessary to discuss a
PH
set-theoretic construction due to Cantor known as the ordinal numbers. We
do not assume that the reader has any previous acquaintance with ordinal
numbers.
The ordinal numbers are best understood as a transfinite extension of
the natural number sequence. The natural number sequence is generated by
starting with 0 and then repeatedly adding 1. If we imagine the natural
number sequence 0, 1, 2, ... as a completed totality, it is reasonable to
posit a new symbol w which is to be regarded as the limit of this
sequence. We can then then continue the sequence by resuming the repeated
addition of 1. Thus we obtain an extended sequence
0, 1, 2, ..., w, w+1, w+2, ....
The same idea can be used to generate further extensions. If we
imagine that the sequence w, w+1, w+2, ... has been similarly completed,
it is reasonable to denote the limit by some such expression as w+w or
w*2. We can then resume the process of adding 1's. This gives
0, 1, 2, ..., w, w+1, w+2, ..., w+w = w*2, w*2+1, w*2+2, ....
Denoting the limit of w*2+1, w*2+2, ..., w*2+n,... by w*3 and
continuing as before, we obtain
0, 1, 2, ..., w, w+1, w+2, ..., w*2, ..., w*3, ..., w*4, ....
2
If we now let w*w = w denote the limit of the subsequence w, w*2,
w*3, ..., w*n, ..., we can continue as before. Thus we have a process of
generating longer and longer extensions of the natural number sequence.
This can be pictured as follows.
0, 1, 2, ..., w, w+1, w+2, ..., w+w = w*2,
2 2 2 2
..., w*3, ..., w*4, ..., w*w = w , ..., w +w = w *2,
3 4 w
..., w , ..., w , ..., w ,
w
w w
w w
..., w , ..., w , ..., e = lim w , ...
0 n n
where by definition e is the limit of the sequence w , w , ...,
0 1 2
w , ... with
n
w \
.
. |
w = . > n.
n w |
w /
Two operations used repeatedly in this process are, first, the addition of
1, and second, the introduction of an expression intended to denote the
limit of a cofinal increasing sequence of previously introduced
expressions. Each of the expressions so generated is called an ordinal
number.
If a and b are ordinal numbers, we write a < b to indicate that
a comes before b in the process of generating the ordinal numbers.
Thus < is an extension of the usual ordering of the natural numbers.
The ordinal numbers which we have introduced fall into three mutually
exclusive classes. Each ordinal number is either 0, a successor ordinal
a+1, or a limit ordinal d = lim d[n] where
n
d[1] < d[2] < ... < d[n] < ....
Operations of ordinal addition and exponentiation are defined in such a
way that a+0 = a, a+(b+1) = (a+b)+1, a+d = lim(a+d[n]), a*1 = a,
n
0 a+1 a d d[n]
a*(n+1) = (a*n)+a, a*w = lim a*n, w = 1, w = w *w, w = lim w .
n n
The account of the ordinal numbers which we have given above is
rather sketchy and imprecise. A rigorous set-theoretic development would
proceed as follows. Let A be a linearly ordered set. We say that A is
well-ordered if every nonempty subset of A has a first element. Two
well-ordered sets which are isomorphic are said to have the same order
type. An ordinal number is then defined to be the order type of any
well-ordered set. This definition permits a convenient set-theoretical
discussion of arithmetical operations on the ordinal numbers. For
instance, if a and b are the order types of the well-ordered sets A
and B respectively, then a+b is defined to be the order type of the
well-ordered set which consists of A followed by B. Similarly a*b is
defined to be the order type of the well-ordered set which results upon
b
replacing each element of B by an isomorphic copy of A. Likewise a is
the order type of the set of functions from B into A with finite
support, ordered by last difference.
Each ordinal number less than e can be uniquely expressed as an
0
exponential polynomial in w. A fairly typical example of an ordinal
number less than e is
0
w+1
w w+1
w + w + w.
This representation in terms of exponential polynomials is known as the
Cantor Normal Form.
We shall now indicate how ordinal numbers can be used to describe the
growth rate of the function f which was defined above in terms of the
PH
Modified Finite Ramsey Theorem. To each ordinal a <=e we shall
0
associate a function f from positive integers to positive integers. As
a
explained above, the ordinal numbers <=e are generated from 0 by
0
repeatedly adding 1 and taking limits of increasing sequences d = lim
n
d[n] where d[1] < d[2] < ... < d[n] < .... We define
f (n) = n + 1,
0
n
f (n) = f f ...f (n) = f (n),
a+1 a a a a
\---v---/
n
f (n) = f (n) for limit ordinals d <=e .
d d[n] 0
Of course this definition presupposes that for each limit ordinal d <=e
0
we have specified an increasing sequence d[1], d[2], ..., d[n], ... such
that d = lim d[n]. We omit the details of exactly how this is done. See
n
for instance the paper by Buchholz and Wainer [7] in this volume.
In order to illustrate the properties of the functions f , a <=e ,
a 0
let us consider the first few of these functions. We have
f (n) = n + 1,
0
f (n) = n + 1 + 1 ... +1 = n + n = 2*n,
1
\-----v------/
n
n n
f (n) = 2*2*...*2*n = 2 *n ~ 2 ,
2
\---v---/
n
n
2 \ 2 \
* | * |
* | * |
f (n) ~ * > n ~ * > n,
3 2 | 2 |
2 / 2 /
and the growth rate of f (n) is already too fast to be described in
4
exponential notation. Note that f has approximately the same growth
3
rate as the Ramsey function f .
R
In general, it can be shown that, for all a < b <=e , f grows
0 b
much faster than f . In particular f is eventually dominated by f
a a b
in the sense that f (n) < f (n) for all sufficiently large n. Thus we
a b
have a hierarchy of fast-growing functions which are indexed by the
ordinal numbers <=e and are ordered by eventual domination. This
0
hierarchy is due to Wainer and is known as the Wainer hierarchy.
We are now in a position to describe the growth rate of the
Paris-Harrington function f which is associated with the Modified
PH
Finite Ramsey Theorem. Namely, it has been shown that the growth rate of
f is approximately the same as that of f . (This result is due to
PH e
0
Paris and Harrington [30] using results of Wainer. See also the papers by
Ketonen-Solovay [21] and Buchholz-Wainer [7] and #6.3 of the monograph by
Graham, Rothschild and Spencer [19].)
In particular f eventually dominates f for all a < e . By
PH a 0
contrast f is eventually dominated by f . Thus f grows much, much
R 4 PH
faster than f .
R
The remarkable aspect of all this is that there is really no way to
describe the growth rate of f except by recourse to ordinal numbers.
PH
Logicians have shown that the ordinal numbers up to and including e are
0
in a sense implicit or unavoidable in the Modified Finite Ramsey Theorem.
This is closely related to the fact that the Modified Finite Ramsey
Theorem cannot be proved in T . (An important classical theorem of
fin
mathematical logic is that e is the limit of the ordinal numbers which
0
are in a certain sense accessible within T .)
fin
#2. Embeddability of finite trees.
------------- -- ------ -----
Our second example of an "unprovable" finite combinatorial theorem
will be concerned with embeddability of finite trees. We begin by
presenting the relevant definitions.
A finite tree is a finite, partially ordered set T such that: (i) T
has a minimum element (called the root of T); (ii) for each x @ T, the
predecessors of x in T are linearly ordered.
Thus a finite tree can be pictured as a diagram which looks like
this:
/ * * *
|
* * * * *
|
* * *
T <
* *
|
| *
\ * <- root of T.
Note that any two elements of a finite tree have a greatest lower bound.
The greatest lower bound of x and y is denoted x /\y.
Let T ant T' be finite trees. An embedding of T into T' is a
one-to-one mapping o: T ->T' such that for all x, y @ T, o(x /\y) =
o(x) /\o(y). (It follows easily that x <=y if and only if o(x) <=
o(y).) We say that T is embeddable into T' if there exists an embedding
of T into T'. We write T\->T' to mean that T is embeddable into T'.
An important result about embeddability of finite trees, due to J. B.
Kruskal [24], is the following. There is no infinite set of pairwise non-
embeddable finite trees. We shall use the following equivalent
formulation of this result.
2.1. KRUSKAL'S THEOREM. For any infinite sequence of finite trees
T , T , ..., T , ..., there exist indices i and j such that i < j and T
1 2 n i
is embeddable into T .
j
Kruskal's Theorem itself is not our promised example of an
"unprovable" finite combinatorial theorem about finite trees. Indeed, the
statement of Kruskal's Theorem involves an infinite sequence and is
therefore definitely not finitary. (Kruskal's Theorem cannot even be
stated in the language of T .) However H. Friedman has shown that
fin
Kruskal's Theorem has a certain consequence which is finitary in its
statement, but not in its proof. This consequence, known as Friedman's
Finite Form, is our promised example.
2.2. FRIEDMAN'S FINITE FORM OF KRUSKAL'S THEOREM. For any positive
integer c, there exists a positive integer n = n which is so large
c
that the following holds. If T , T , ..., T is any finite sequence of
1 2 n
finite trees with |T | <=c*i for all i <=n, then there exist indices i
i
and j such that i < j <=n and T \->T .
i j
Clearly Friedman's Finite Form is a finitary statement, referring
only to finite sets and structures. Hence Friedman's Finite Form can be
stated within T . The following unprovability theorem is due to
fin
Friedman (198l, unpublished). For a full exposition of the theorem and
its proof, see Simpson [37].
2.3. THEOREM. Friedman's Finite Form of Kruskal's Theorem is not
provable in T . In other words, Friedman's Finite Form of Kruskal's
fin
Theorem cannot be proved by finite combinatorial methods alone.
In this result, the bound of c*i can be strengthened considerably.
See Loebl-Matousek [26] (this volume) and Smith [39].
Let me now indicate how Friedman's Finite Form can be derived from
Kruskal's Theorem. Suppose for a contradiction that Friedman's Finite
Form is false. Let V be the set of all finite sequences <T ,T ,...,T >
c 1 2 n
such that |T | <=c*i for all i <=n, and T \->T for no i and j with i <
i i j
j <=n. Then for some c, V is infinite. If we partially order this V
c c
by extension, we see that it is an infinite, finitely branching tree.
"
Hence by Konig's Infinity Lemma [23], it has an infinite path. In other
words, there is an infinite sequence of finite trees <T ,T ,...,T ,...>
1 2 n
such that |T | <=c*i for all i, and T \->T for no i and j with i < j.
i i j
This contradicts Kruskal's Theorem.
"
In the above derivation, it is interesting to note how Konig's Lemma
"
was applied in a non-traditional way. Traditionally, Konig's Lemma is
used to derive infinitistic theorems from finitistic ones. For example
"
Konig's Lemma can be used to deduce the infinite form of Dilworth's
"
Theorem from the finite form. Indeed, the title of Konig's paper [23]
translates to: "On a method of drawing conclusions from the finite to the
"
infinite." This means that Konig must have viewed his lemma as a one-way
pipeline from the finite to the infinite. However, there is no reason not
to reverse the flow and derive finitistic statements from infinitistic
ones. Such was the procedure of the previous paragraph.
By Theorem 2.3, Friedman's Finite Form cannot be proved without some
use of infinite sets. Actually Friedman obtained a much stronger result.
Namely, neither Kruskal's Theorem nor Friedman's Finite Form can be proved
without at least some weak use of uncountable sets. (The precise result
is that Friedman's Finite Form cannot be proved in the formal system ATR .
0
For a proof and references to the literature, see Simpson [37].) Thus
Friedman's Finite Form of Kruskal's Theorem is, so to speak, even more
unprovable than the Modified Finite Ramsey Theorem!
This higher degree of unprovability is reflected in the associated
growth rate. Using the notation n as in the statement of Friedman's
c
Finite Form, it is natural to ask the following question. How fast does
n grow as a function of c? The answer is that n grows faster than
c c
the Wainer function f where G is a certain ordinal number which is
G 0
0
much, much larger than e . In order to define G , let OR be the class
0 0
of all ordinal numbers and consider the following hierarchy of continuous
increasing functions h : OR ->OR where a ranges over OR. Given b @ OR
a
b th
we define h (b) = w and, for all a > 0, h (b) = the b simultaneous
0 a
fixed point of the functions h , a' < a. Then G is defined to be the
a' 0
least ordinal g > 0 such that h (b) < g for all a, b < g. This is a
a
very large ordinal number. By comparison e = h (0) is miniscule. The
0 1
Wainer hierarchy can be extended through the ordinals <=G . It can then
0
be shown that f is eventually dominated by the Friedman function n (as
G c
0
a function of c). Indeed, it can be shown that the Friedman function
eventually dominates f for certain ordinals a which are somewhat
a
larger than G .
0
What about n for small values of c? This question points to
c
another remarkable aspect of Friedman's Finite Form. Consider for
instance c = 12. Please bear in mind that n is a single, specific
12
positive integer. (Namely, it is the smallest positive integer n with
the property that, in any sequence of finite trees T , T , ..., T with
1 2 n
|T | <=12*i for all i <=n, there is at least one embedding T \->T , i <
i i j
j <=n.) Hence the existence of n can be proved in T . However, it
12 fin
turns out that n is extremely large. It can be shown that n is much
12 12
larger than
2 \
* |
* |
* > 1000
2 |
2 / .
In fact, Friedman has shown that any proof of the existence of n within
12
T would require more than
fin
2 \
* |
* |
* > 1000
2 |
2 /
sheets of paper! Hence there is no hope for a manageable proof of the
existence of n within T . (For details see Smith [39].) This version
12 fin
of Theorem 2.3 is interesting from the viewpoint of ultrafinitism.
#3. Exponential notation.
----------- --------
Our third example of an "unprovable" finitistic theorem is number-
theoretical rather than combinatorial. The theorem is concerned with one
of the most elementary number-theoretic concepts, namely base b
notation. (The special case b = 10 is the usual decimal notation.)
Let b be a positive integer >=2. Any nonnegative integer n can
be written uniquely in the form
n n
1 k
n = b *c + ... + b *c
1 k
where k >=0, n > ... > n >=0, and 0 < c < b for i = 1, ..., k.
l k i
This is known as the base b representation of n. For example the base 2
representation of 266 is
8 3
266 = 2 + 2 + 2.
We may extend this by writing each of the exponents n , ..., n in
1 k
base b notation, then doing the same for each of the exponents in the
resulting representations, ... until the process stops. This yields the
so-called complete base b representation of n. For example the complete
base 2 representation of 266 is obtained as:
8 3
266 = 2 + 2 + 2
3
2 2+1
= 2 + 2 + 2
2+1
2 2+1
= 2 + 2 + 2.
We now present the definitions which are needed to state the third
"unprovable" theorem. Let R (n) be the nonnegative integer which
b
results if we take the complete base b representation of n and then
replace each b by b+1. Thus R is a "base change" function. For
b
example
3+1
3 3+1
R (266) = 3 + 3 + 3.
2
For each nonnegative integer n we recursively define a sequence of
nonnegative integers (n) , (n) , ..., (n) , ... by
0 1 k
(n) = n,
0
/ R ((n) ) - 1 if (n) > 0,
| k+2 k k
|
(n) = <
k+1 |
|
\ 0 if (n) = 0,
k
for all k >=0. This is known as the Goodstein sequence beginning with
n. For example the Goodstein sequence beginning with 266 is
2+1
2 2+1
(266) = 266 = 2 + 2 + 2,
0
3+1
3 3+1
(266) = 3 + 3 + 3 - 1
1
3+1
3 3+1
= 3 + 3 + 2,
4+1
4 4+1
(266) = 4 + 4 + 1,
2
5+1
5 5+1
(266) = 5 + 5 ,
3
6+1
6 6+1
(266) = 6 + 6 - 1
4
6+1
6 6 5
= 6 + 6 *5 + 6 *5 + ... + 6*5 + 5,
7+1
7 7 5
(266) = 7 + 7 *5 + 7 *5 + ... + 7*5 + 4,
5
.
.
.
.
We can see that the Goodstein sequence beginning with 266 appears
initially to increase very rapidly. Nevertheless, despite appearances, it
can be proved that this sequence converges to 0. In other words, (266) =
k
0 for all sufficiently large k. This surprising conclusion is due to
Goodstein [18] who actually proved the same result for all Goodstein
sequences:
3.1. GOODSTEIN'S THEOREM. For all n there exists k such that (n) =
k
0. In other words, every Goodstein sequence converges to 0.
Obviously the statement of Goodstein's Theorem is totally finitistic,
referring only to natural numbers and elementary operations on them. On
the other hand, we shall see that Goodstein's proof of his theorem is
definitely not finitistic. Moreover Kirby and Paris [22] have shown that
no finitistic proof of the theorem is possible. Thus Goodstein's Theorem
will turn out to be our promised example of an "unprovable" number-
theoretic theorem.
I shall now sketch the proof of Goodstein's Theorem. The proof is
infinitistic in that it makes direct use of the ordinal numbers up to e .
0
w
Given b >=2 and any natural number n, we denote by R (n) the result
b
of taking the complete base b representation of n and replacing each
w
occurrence of b by w. Thus R (n) is the Cantor Normal Form of some
b
ordinal number less than e . For example
0
w+1
w w w+1
R (266) = w + w + w.
2
w w w
Note that R (m) < R (n) if and only if m < n. Also R (0) = 0, and
b b b
w w
R (n) = R R (n). Now given n, consider the Goodstein sequence
b b+1 b
(n) , (n) , ..., (n) , (n) , ...
0 1 k k+1
and the corresponding sequence of ordinal numbers
w w w w
R ((n) ), R ((n) ), ..., R ((n) ), R ((n) ), ....
2 0 3 1 k+2 k k+3 k+1
For all k such that (n) > 0, we have
k
w w
R ((n) ) = R (R ((n) )-1)
k+3 k+1 k+3 k+2 k
w
< R (R ((n) )
k+3 k+2 k
w
= R ((n) ).
k+2 k
Since there is no infinite descending sequence of ordinal numbers, it
follows that (n) = 0 for some k. This completes the proof.
k
We now state the following unprovability theorem due to Kirby and
Paris.
3.2. THEOREM (Kirby-Paris [22]). Goodstein's Theorem 3.1 is not
provable in T . In other words, Goodstein's Theorem cannot be proved
fin
by finite combinatorial methods alone.
This gives our third example of an "unprovable" finite combinatorial
theorem. As in the case of our other two examples, the "unprovability" is
reflected in the very rapid growth rate of a certain function. For all n
let f (n) be the smallest k such that (n) = 0. Kirby and Paris have
G k
shown that the Goodstein function f grows approximately as fast as
G
f . In particular f eventually dominates f for all a < e . (An
e G a 0
0
extremely elegant, computational proof of these results has been given by
Cichon [10]. See also Buchholz and Wainer [7].)
#4. Appendix
--------
In this section I shall discuss various developments which are
related to the results of ##1-3.
* * *
Ramsey's Theorem is only the beginning of a highly developed field of
research. For an excellent but by now somewhat dated survey of this
rapidly changing field, see the monograph Ramsey Theory by Graham,
Rothschild, and Spencer [19]. I want to discuss some results in Ramsey
Theory which have some bearing on "unprovable" finite combinatorial
theorems.
One of the best-known generalizations of Ramsey's Theorem is the
" '
Canonical Ramsey Theorem due to Erdos and Rado (see # 5.5 of [19]).
Recently Kanamori and McAloon [20] have used the Canonical Ramsey Theorem
to give an elegant alternative to the results of Paris and Harrington.
k
For any set X of positive integers, a coloring f: [X] ->X is said to be
k
regressive if f(F) < min(F) for all F @ [X] such that min(F) > 1.
The Kanamori-McAloon version of the Modified Finite Ramsey Theorem reads
as follows.
4.1. THEOREM. For all k and m there exists n so large that, for all
k
regressive f: [X] ->X = {1,2,...,n}, there exists Y <=X such that |Y| >=m
k
and, for F @ [Y] , f(F) depends only on min(F).
Kanamori and McAloon have shown that this statement has the same
logical and growth-rate properties as the Paris-Harrington statement 1.2.
In particular, the Kanamori-McAloon statement is not provable in T .
fin
The advantage of this approach is that the proof of the Kanamori-
McAloon unprovability result is much simpler than the proof of the
corresponding Theorem 1.3 of Paris and Harrington. To those who wish to
present a version of the Paris-Harrington result in a first-year graduate
logic course but do not want to spend too much time on the combinatorial
details, I recommend the first part of Kanamori-McAloon [20].
* * *
In recent years there have appeared a number of infinitistic Ramsey-
type theorems which are topological in nature. The prototypical result of
this kind is the following theorem due to Galvin and Prikry. For any
oo
infinite set X, let [X] be the set of all infinite subsets of X. We
oo
regard [X] as a topological space with basic open sets of the form
X oo
O = {Y @ [X] : F <=Y and G /\Y = O}
FG
where F and G are disjoint finite subsets of X.
4.2. GALVIN-PRIKRY THEOREM ([17]). Let X be an infinite set. If
oo oo
[X] = C U ... U C with each C closed, then there exists Y @ [X] such
1 l i
oo
that [Y] <=C for some i.
i
oo
(The hypothesis that each C be a closed subset of [X] can be
i
weakened considerably. For instance, Galvin and Prikry proved their
theorem with "closed" replaced by "Borel." The sharpest result in this
direction is due to Ellentuck. For details see [9].)
Friedman, McAloon and Simpson [15] have shown that, despite its
infinitary nature, the Galvin-Prikry Theorem 4.2 is relevant to finite
combinatorics. Indeed, Theorem 4.2 can be converted into a finitary
statement, just as Paris and Harrington converted the Infinite Ramsey
Theorem 1.4 into the Modified Finite Ramsey Theorem 1.2. (More precisely,
the miniaturization procedure of [15] is modeled on the original idea of
Paris [29] rather than on Paris-Harrington [30].) This finitary statement
due to Friedman, McAloon and Simpson turns out to be unprovable not only
in T but also in the much stronger theory ATR which was mentioned near
fin 0
the end of #2. In addition, the associated fast-growing function grows at
about the same rate as f . (These results are sharp in the sense that
G
0
ATR is the weakest natural subsystem of second order arithmetic in which
0
4.2 is provable. For details see [15].)
As mentioned above, the Galvin-Prikry Theorem has served as the
prototype for a large number of extensions and generalizations of the
Infinite Ramsey Theorem. A comprehensive survey of this area can be found
in [9]. Let me describe only one of these results, due to Carlson and
Simpson [8]. For any set X, a partition of X is a pairwise disjoint
collection of nonempty subsets of X whose union is all of X. If X is
oo
infinite, let (X) be the set of all infinite partitions of X. For any Y
oo
@ (X) , put
oo oo
(Y) = {Z @ (X) : Z is coarser than Y}.
oo
We regard (X) as a topological space with basic open sets of the form
X oo
O = {Y @ (X) : Y|F = P}
P
where: P is a partition of a finite subset F of X; Y|F is the restriction
of Y to F, i.e. Y|F = {y /\F: y @ Y and y /\F !=O}.
4.3. DUAL GALVIN-PRIKRY THEOREM (Carlson and Simpson [8]). Let X
oo
be an infinite set. If (X) = C U ... U C with each C closed, then
1 l i
oo oo
there exists Y @ (X) such that (Y) <=C for some i.
i
(As in the case of Theorem 4.2, the hypothesis "C closed" in Theorem
i
4.3 can be weakened considerably. For details see [8].)
In view of the results of Friedman, McAloon and Simpson which were
discussed above, it is natural to ask whether Theorem 4.3 has any finite
combinatorial consequences which are unprovable in relatively strong
subsystems of second order arithmetic. (This was my original motivation
for formulating the Dual Galvin-Prikry Theorem. See #7 of [8].) Almost
nothing is known about this question. It is known that Theorem 4.2 can be
deduced from Theorem 4.3 as an easy corollary. Hence by [15] the growth
rate associated to Theorem 4.3 is at least as great as f . However, it
G
0
is not known to be any greater. Similarly, almost nothing is known about
the following, closely related, axiomatic question. What set existence
axioms are needed to prove Theorem 4.3? It follows from [15] that at
least the axioms of ATR are needed, and it is reasonable to conjecture
0
that much more is needed, but this conjecture remains open. Analogous
remarks could be made about the other generalizations and extensions of
the Galvin-Prikry Theorem which are discussed in [9].
(Note added January 31, 1986. Recent work of Blass, Hirst and
---- ----- ------- --- ----
Simpson [4] yields some non-trivial upper bounds on the set existence
axioms and growth rates associated with Hindman's Theorem and the Dual
Galvin-Prikry Theorem. However, more work remains to be done.)
* * *
A large part of modern Ramsey Theory is concerned with the following
theorem of van der Waerden. Let N be the set of nonnegative integers. A
finite arithmetical progression is a subset of N of the form
{a, a + d, a + 2*d, ..., a + k*d}.
4.4. VAN DER WAERDEN'S THEOREM. If N = C U ... U C then, for
1 l
some i, C contains arbitrarily long finite arithmetical progressions.
i
A equivalent statement of Van der Waerden's Theorem reads as follows.
For any k and l, there exists n so large that, if {1, 2, ..., n} = C U
1
... U C , then for some i, C contains an arithmetical progression of
l i
length k. Define W (k) to be the smallest n such that this conclusion
l
holds. In view of #1, it is natural to ask: What is the growth rate of
W (k) as a function of l and k?
l
The currently known upper bound for W (k) is something like the
l
Ackermann function, i.e. the function f of #1. The problem of improving
w
this bound is open, famous, and apparently difficult. (See for instance
the paper by Brackin [5] in this volume.)
It is unknown whether W (k) is eventually dominated by f (k) for any
2 n
fixed n. Should this turn out not to be the case, an interesting
unprovability result would follow. Namely, it would follow that Van der
+
Waerden's Theorem is not provable in the formal systems WKL and WKL of
0 0
+
[38]. This would be interesting because WKL and WKL are known to be
0 0
adequate for the development of a large part of ordinary mathematics.
Thus we would be able to conclude that any proof of Van der Waerden's
Theorem must use strong methods which go beyond those that are usually
needed in mathematics.
For instance, the standard combinatorial proof of Van der Waerden's
Theorem uses a strong method known as double induction. For each fixed k,
the existence of W (k) is proved by induction on l assuming the existence
l
of W (k') for all k' < k and all l'. This type of induction is
l'
+
unavailable in WKL and WKL and is rarely needed in mathematical
0 0
practice. The interesting problem is whether all proofs of Van der
Waerden's Theorem must necessarily involve such unusual methods.
Similar remarks apply to the theorems of Hales-Jewett, Graham-Leeb-
'
Rothschild, and Szemeredi. (For an exposition of these theorems, see
Chapter 2 of [19].) Each of these theorems is a generalization of Van der
Waerden's Theorem. In each case, the corresponding growth rate is not
known to be eventually dominated by f for any finite n, and it would be
n
very interesting if it were not so dominated.
* * *
Furstenberg and his coworkers (see [16]) have developed a beautiful
approach to Van der Waerden's Theorem and related results. Namely, they
have shown that such results can often be deduced from general theorems of
topological dynamics and ergodic theory. (In some cases, the process can
be reversed so that the combinatorial theorems are in fact interchangable
with their dynamical counterparts.) Thus Furstenberg and his coworkers
have provided a sort of analytical or perhaps geometrical context for this
branch of combinatorics. See for instance the paper by Bergelson [3] in
this volume.
From our viewpoint here, Furstenberg's approach is intriguing because
it introduces, into finite combinatorics, methods which appear to be
highly abstract and set-theoretical. For instance, Furstenberg's proof of
'
Szemeredi's Theorem (Chapter 7 of [16]) uses a complicated structural
analysis of measure-preserving transformations. This seems to require a
heavy dose of transfinite induction. Similarly, the Furstenberg-Weiss
proof of Hindman's Theorem (Chapter 8 of [16]) involves Zorn's Lemma
applied to a non-metrizable Tychonoff product space. (See the proof of
Lemma 8.4 in [16].) Developments such as these raise the question of
whether the highly abstract methods are ever really needed in order to
prove particular combinatorial theorems. If they are in fact needed, then
this would probably lead to some results concerning unprovability and
fast-growing functions. Unfortunately, at the present time, there is
nothing but speculation here.
(Note added January 31, 1986. Recent research of Blass, Hirst and
---- ----- ------- --- ----
Simpson [4] seems to indicate that highly abstract, set-theoretical
methods are less essential for the study of dynamical systems than they
might at first appear to be. For instance, the main results of Chapter 8
of [16], including the Auslander-Ellis Theorem 8.7, can be proved in a
+
relatively weak subsystem of second order arithmetic known as ACA .
0
However, the question of which set existence axioms are needed to prove
'
Szemeredi's Theorem is still open.)
* * *
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 quasi-ordering is
a set Q (usually infinite) together with a binary relation <=which is
reflexive and transitive on Q. A well-quasi-ordering is a quasi-ordering
Q with the property that, for every infinite sequence <Q : n @ N> 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.
