FOM: 29:Large Cardinals/where are we? I

[Harvey Friedman]

This is the 29th in a series of self contained postings to fom covering a
wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM
5:Constructions  11/15/97  5:24PM
6:Undefinability/Nonstandard Models   11/16/97  12:04AM
7.Undefinability/Nonstandard Models   11/17/97  12:31AM
8.Schemes 11/17/97    12:30AM
9:Nonstandard Arithmetic 11/18/97  11:53AM
10:Pathology   12/8/97   12:37AM
11:F.O.M. & Math Logic  12/14/97 5:47AM
12:Finite trees/large cardinals  3/11/98  11:36AM
13:Min recursion/Provably recursive functions  3/20/98  4:45AM
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM
15:Structural Independence results and provable ordinals  4/16/98
10:53PM
16:Logical Equations, etc.  4/17/98  1:25PM
16':Errata  4/28/98  10:28AM
17:Very Strong Borel statements  4/26/98  8:06PM
18:Binary Functions and Large Cardinals  4/30/98  12:03PM
19:Long Sequences  7/31/98  9:42AM
20:Proof Theoretic Degrees  8/2/98  9:37PM
21:Long Sequences/Update  10/13/98  3:18AM
22:Finite Trees/Impredicativity  10/20/98  10:13AM
23:Q-Systems and Proof Theoretic Ordinals  11/6/98  3:01AM
24:Predicatively Unfeasible Integers  11/10/98  10:44PM
25:Long Walks  11/16/98  7:05AM
26:Optimized functions/Large Cardinals  1/13/99  12:53PM
27:Finite Trees/Impredicativity:Sketches  1/13/99  12:54PM
28:Optimized Functions/Large Cardinals:more  1/27/99  4:37AM
28':Restatement  1/28/99  5:49AM

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of self contained postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html The published
state of the art for discrete/finite independence results from ZFC is in
the following article that has just appeared:

[1] H. Friedman, Finite Functions and the Necessary Use of Large Cardinals,
Annals of Mathematics, Vol. 148, No. 3 (November, 1998), pp. 803--893.

There is a followup paper which has been submitted for publication:

[2] H. Friedman, Finite Trees and the Necessary Use of Large Cardinals,
March 22, 1998, 58 pages, to appear.
http://www.math.ohio-state.edu/foundations/manuscripts.html

In fact, [2] builds in an essentially manner on practically the whole of
[1]. The independent statements in [2] are yet more well motivated than
those in the Annals of Math paper, in light of their close ties with the
idea of "greedy constructions" that figures so prominently in computer
science.

I got interested in disguising the greedy constructions used in [2]. I
found some yet more natural kinds of greedy constructions, and chose to
state the associated independent statements without mentioning the
underlying greedy constructions. This is in the FOM posting:

[3] H. Friedman, 28:Optimized Functions/Large Cardinals:more  1/27/99
4:37AM.  28':Restatement 1/29/99  11:47AM.
http://www.math.ohio-state.edu/foundations/manuscripts.html

One of the reasons that I endeavored to get rid of explicit mention of
greedy constructions is that I wanted a form of the independence results
that is more attractive than [2] even for mathematicians who don't find
inductive constructions very natural. Of course, it is hard to avoid
inductive constructions of finite length in just about any area of
mathematics - but it is often more of a matter of technical constructions
in lemmas, rather than the main event. In contrast, inductive constructions
are obviously more of a main event in computer science - especially in the
theory of algorithms.

But now there has been a strong development in another kind of
discrete/finite independence results which has a number of advantages.
These are not based on inductive constructions - at least in the same
sense. This new development has changed the picture as far as I am
concerned.

So here is the plan:

a. I will be continuing the development of necessary uses of large
cardinals for greedy constructions. The ideas in [3] will be restated in
posting 30:Large Cardinals/where are we? II, in terms of greedy
constructions. This is the first of two main branches jumping off of [1].
This development depends on [1] in essentially its entirety - as does [2].

b. The results stated below constitute the new, second main branch jumping
off of [1]. There is substantial overlap with [1], but some of the delicate
points in [1] can be avoided. And there are substantial additional
technical ideas not present in [1].

c. My overall assessment is that both of these branches are equally
important, and have equal promise. The first branch is probably more
attractive to computer scientists, whereas the second branch is probably
more attractive to the general mathematics community.

d. It goes wihtout saying that this assessment may change as circumstances
warrant.

e. Recall my FOM posting, "Perfect" statements, 2/5/99  2:46AM. That is
currently my gold standard against which both of these two branches jumping
off of [1] are to be ultimately measured. I am confident that both of these
two branches represent substantial progress towards acheiving that gold
standard.

******

Now for the second main branch jumping off of [1]. I had these ideas for
some time, with an independence result involving infinite sets of natural
numbers. Although the statement is finitary in the sense that it follows
from the 1-consistency of Mahlo cardinals of finite order, and implies the
consistency of Mahlo cardinals of finite order, I have struggled for some
time with the problem of giving an appropriate finite form. The finite
forms did not, until now, compare favorably with the finite statements in
[1] - [3]. But now it looks like I have quite convincing finite forms.

I now want to motivate the key concept of R-extension that drives the
results. The following is a beautiful exercise for undergraduates:

THEOREM 1. Let k >= 1 and R containedin N^k. There exists a unique set A
containedin N such that for all x in N, x in A if and only if x is not
related by R to any z_1,...,z_k-1 < x from A.

[More formally, for all x in N, x in A if and only if (for all
z_1,...,z_k-1 in A)(if z_1,...,z_k-1 < x then notR(x,z_1,...,z_k-1))].

Theorem 1 is a neat encapsulation of definition by recursion on N = the
nonnegative integers.

Note that we cannot conclude that A is infinite. In fact, there is really
no structure theory for these unique A's since the unique A may be any
subset of N that includes 0.

However, we can relax the condition so that we can get A to be infinite;
however, we do lose uniqueness:

THEOREM 2. Let k >= 1 and R containedin N^k. There exists an infinite set A
containedin N such that for all x,y in A, x+y in A if and only if x is not
related by R to any z_1,...,z_k-1 < x from A.

There could well be an interesting structure theory already for this
notion. I'm not sure. However, we now consider a stratified notion that is
obviously closely related.

DEFINITION. Let k >= 1, R containedin N^k and A,B containedin N. We say
that B is an R-extension of A if and only if
	i) A containedin B;
	ii) for all x,y in A, x+y in B if and only if x+y is not related by
R to any z_1,...,z_k-1 < x+y from B.

Then we can restate Theorem 2 as follows: For all R there is an infinite A
such that A is an R-extension of A.

We now define the crucial notion of R-tower.

DEFINITION. Let k >= 1 and R containedin N^k. An R-tower is a nonempty
sequence of subsets of N, finite or infinite in length, such that each term
(except the first) is an R-extension of the preceding term. An R-tower is
said to be finite if and only if its length is finite and its last term is
finite.

The most basic structure theory of R-towers corresponds to formal systems
from logic, ranging from fragments of set theory, to ZFC, to large cardinal
axioms going well beyond the usual axioms of set theory!

For background, we first relate infinite towers to self R-extensions. The
following is straighforward:

THEOREM 3. Let k >= 1, R containedin N^k, and A containedin N. The
following are equivalent:
	i) A is an R-extension of A;
	ii) A is the union of an R-tower of infinite length.

The real excitement concerns R-towers of finite length. Here is the first
independence result:

PROPOSITION 4. Let k,n >= 1 and R containedin N^k. There is an R-tower of
length n whose first term contains infinitely many odd integers. In fact,
for all infinite E containedin N, there is an R-tower of length n whose
first term contains infinitely many elements from E and also 1.

THEROEM 5. In RCA_0, Proposition 4 (both forms) follows from the
1-consistency of ZFC + {there exists an n-Mahlo cardinal}_n and implies the
consistency of ZFC + {there exists an n-Mahlo cardinal}_n. Proposition 4
(both forms) is provably equivalent in RCA_0 to a pi-0-2 sentence.

What has eluded me for some time is a really good way of getting a finite
form for Proposition 4. The nicest way is to give a finite form for a
related Proposition which has the same metamathematical properties.

DEFINITION. Let k >= 1, R containedin N^k, and S = S[1],...,S[n] be an
R-tower. The initial segments of S are the n-tuples of the form S[1]
intersect [0,x),...,S[n] intersect [0,x), where x in S[1]. Thus there is a
unique initial segment of S corresponding to each element of S[1], and so
the number of initial segments of S is one more than the cardinality of
S[1].

PROPOSITION 6. Let k,n >= 1 and R containedin N^k. There is an R-tower of
length n with infinite first term such that some nonempty initial segment
is an R-tower. In fact, there is an R-tower of length n with infinite first
term, all of whose initial segments are R-towers.

THEROEM 7. In RCA_0, Proposition 4 (both forms) follows from the
1-consistency of ZFC + {there exists an n-Mahlo cardinal}_n and implies the
consistency of ZFC + {there exists an n-Mahlo cardinal}_n. Proposition 4
(both forms) is provably equivalent in RCA_0 to a pi-0-2 sentence.

Proposition 6 has very intersting finite forms.

PROPOSITION 8. Let k,n >= 1 and R containedin N^k. There is a finite
R-tower of length n whose first term has cardinality 1, where the sole
initial segment is a an R-tower whose second term is nonempty.

PROPOSITION 9. Let k,n,m >= 1 and R containedin N^k. There is a finite
R-tower of length n whose first term has cardinality m, where all of the
initial segments are R-towers.

Let ATR(<lambda) be arithmetic transfinite recursion on every ordinal <
lambda. We will only consider the case where lambda is a specific ordinal
<= omega^2. There are several formulations of ATR(<lambda). E.g., there is
a light faced version and a bold faced version. Also, one can have
restricted induction or full induction. It doesn't matter for the results.

THEOREM 10. In RCA_0, Proposition 8 is provably equivalent to the
consistency of ATR(<omega+omega). In RCA_0, Proposition 8 is provably
equivalent to the consistency of ATR(<omega^2).

It is obvious that Propositions 8 and 9 have straightforward pi-0-2
equivalents by compactness. I.e., let t >> k,n,m >= 1 and R containedin
[0,t]^k. There is an R-tower .... and whose last term is contained in [0,t].

But these Propositions are even more concrete. The >> can be put in
explicit form using iterated exponentials, resulting in pi-0-1 sentences!
There is an especially convenient way to do this:

PROPOSITION 11. Let k,n >= 1 and R containedin N^k be finite. There is an
R-tower of length n whose first term has cardinality 1, where the sole
initial segment is an R-tower, whose last term consists of integers below
the exponential stack of 8kn 2's.

PROPOSITION 12. Let k,n,m >= 1 and R containedin N^k be finite. There is an
R-tower of length n whose first term has cardinality m, where all of the
initial segments are R-towers, whose last term consists of integers below
the exponential stack of 8knm 2's.

Note that these are explicitly pi-0-1. Furthermore, they have the same
metamathematical properties as Propositions 8 and 9. In fact, we can use
the base theory EFA = exponential function arithmetic.

Of course, ATR(<omega^2) is much less than a tiny speck of dust on ZFC, or
even impredicative systems like ATR. But now we put a cardinality condition
on the initial segments.

PROPOSITION 13. Let k,n,m, >= 1 and R containedin N^k. There is a finite
R-tower of length n whose first term has cardinality m, and whose initial
segments are R-towers of cardinalities
(kn)!!!,(2kn)!!!,(3knm)!!!,(4mkm)!!!,...,(mknm)!!!.

Note the funny estimates here, where m only starts appearing at the third
term. It will be clear below why I did this.

THEOREM 14. In RCA_0, Proposition 13 is provably equivalent to the
consistency of Russell's finite theory of types, or Zermelo set theory with
bounded separation.

We again see that this is obviously equivalent to a pi-0-2 sentence by
compactness. We can also give the explicit estimate involving interated
exponentials, in direct analogy with Propositions 11 and 12.

Now let's get rid of the m's in thsse estimates:

PROPOSITION 15. Let k,n,m >= 1 and R containedin N^k. There is a finite
R-tower of length n whose first term has cardinality m, whose initial
segments are R-towers of cardinalities
(kn)!!!,(2kn)!!!,(3kn)!!!,(4kn)!!!,...,(mkn)!!!.

THEOREM 16. In RCA_0, Proposition 15 is provably equivalent to the
consistency of ZFC + {there exists an n-Mahlo cardinal}_n.

Again, this is obviously equivalent to a pi-0-2 sentence by compactness.
And we can also give the explicit estimate involving iterated exponentials,
in direct analogy with Propositions 11 and 12. We can use EFA as the base
theory. Thus we have presented necessary uses of large cardinals for
explicitly pi-0-1 sentences.