FOM: 14:New characterizations of the provable ordinals

[Harvey Friedman]

This is the 14th in a series of positive 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

A complete archiving of fom, message by message, is available at
http://www.math.psu.edu/simpson/fom/
Also, my series of positive postings (only) is archived at
http://www.math.ohio-state.edu/foundations/manuscripts.html

We present a simple set theoretic characterization of the provable ordinals
of set theory. The provable ordinals of a theory T which contains RCA_0 is
defined as the ordinals alpha for which there is a presentation of a
primitive recursive relation on N of order type alpha such that T proves
that this presentation defines a well ordering on N. We denote the least
ordinal greater than all provable ordinals of T is normally denoted by o(T).

There are some basic facts indicating how robust this notion is. First of
all, if T is a consistent r.e. theory then o(T) is a recursive ordinal.
Obviously, if T is inconsistent then this ordinal is Church-Kleene omega_1,
which is not a recursive ordinal. This result can be strengthened to allow
T to be a Sigma-1-1 theory.

Secondly, if T contains ACA_0 we can allow arithmetically defined relations
for the provable ordinals, and get the same provable ordinals. Thirdly, we
can go even further: if T contains ATR_0 then we can even allow Sigma-1-1
defined relations for the provable ordinals, and also get the same provable
ordinals. Again, T may be any Sigma-1-1 theory.

It is well known that o(RCA_0) = omega^omega, o(ACA_0) = o(PA) = epsilon_0,
and o(ATR_0) = Gamma_0.

1. RELATIONAL EQUATIONS

Let R containedin A^2 and E containedin A. We write R[E] = {y: there exists
x such that R(x,y)}. Let (A,<) be a linear ordering. We write R_<[E] = {y:
there exists x < y such that R(x,y)}.

We wish to consider the relational equation E = A\R_<[E], where (A,<) is a
linear ordering and R containedin A^2.

THEOREM 1.1. Let (A,<) be a linear ordering. The following are equivalent.
	i) for all R contianedin A^2, E = A\R_<[E] has a solution;
	ii) for all R containedin A^2, E = A\R_<[E] has a unique solution;
	iii) (A,<) is a well ordering.

We also want to consider a multidimensional generalization of the
relational equations E = R_<[A\E]. Let (A,<) be a linear ordering and k,n
>= 1. For x,y in A^k, we write x < y if and only if max(x) < max(y). Let R
containedin A^2k and E containedin A^k. We write R[E] = {y in A^k: there
exists x such that R(x,y)}. We write R_<[E] = {y in A^k: there exists x < y
such that R(x,y)}.

We now consider relational equations E = R_<[A^k\E]. Here the dimensions
match: E is k-dimensional and R is 2k-dimensional.

THEOREM 1.2. Let (A,<) be a linear ordering and k >= 1. The following are
equiavlent.
	i) for all R contianedin A^2, E = R_<[A\E] has a solution;
	ii) for all R containedin A^2k, E = R_<[A^k\E] has a unique solution;
	iii) (A,<) is a well ordering.

2. LOGICAL EQUATIONS

For our purposes, a Boolean form is a propositional combination of
inequalities between variables, x_i < x_j. For this purpose, we use
variables x_1,x_2,..., the formal symbol <, and the usual logical
connectives &, v, not, -->. A Boolean form in {x_1,...,x_n} is a Boolean
form all of whose variables are among those shown.

The purpose of these Boolean forms is to specify a particular relation on
every linear ordering in a uniform way. Thus if R is a Boolean form in
x_1,...,x_n and (A,<) is a linear ordering, then we write R_A for
{(x_1,...,x_n) in A^n: R(x_1,...,x_n)}.

We can now consider logical equations of the form E = R_A<[A^k\E]. Here R
is a Boolean form in x_1,...,x_k, and A,E are unknowns. Thus a solution to
the logical equation is a system (A,<,E), where (A,<) is a linear ordering
and E containedin A^k. Technically speaking, we should write E =
(R_A)_<[A^k\E], but we omit the parentheses.

We now give a background theorem of independent interest.

THEOREM 2.1. A set of ordinals is constructible if and only if it is a
cross section of some solution to some logical equation whose linear
ordering is an ordinal under epsilon.

A linear ordering is said to be normal if and only if some initial segment
is N under its usual ordering. We say that (A,<,E) is normal if and only if
(A,<) is normal.

Let K be a class of systems (A,<,E) and X be a logical equation. We define
the crucial binary relation S = S[K,X] on N^k-1 as follows. S(x,y) if and
only if for all normal solutions (A,<,E) of X in K, the least z such that
E(x,z) is < the least w such that E(y,w). Thus S(x,y) implies there exists
z,w such that E(x,z) and E(y,w).

A binary relation S is said to be strictly well founded if and only if
S(x_2,x_1),S(x_3,x_2),S(x_4,x_3),... is impossible. If S is strictly well
founded then we construct the unique map f:N --> On by f(n) = the least
ordinal greater than all f(m) such that S(m,n). We then define the ordinal
of S as the least ordinal greater than all values of f.

We now associate an ordinal to K. We write ord(K) for the least ordinal
greater than the ordinal of all strictly well founded S[K,X].

Sometimes K depends only on (A,<) and not on E. To reflect this, let M be a
class of linear orderings and X be a logical equation. We define S[M,X] =
S[K,X], where K is the class of all systems whose linear ordering lies in
M.

The cardinality of a limit point in a linear ordering is defined to be the
cardinality of the set of its predecessors. We now define several classes
of linear orderings. Let kappa be an uncountable cardinal.

M1(kappa): cardinality kappa, and with a countable limit point.
M2(kappa): M1(kappa) and every proper initial segment has cardinality < kappa.
M3(kappa): M2(kappa) and there is a closed unbounded set of order type kappa.

THEOREM 2.2. The minimum value of ord(M1(kappa)) = the minimum value of
ord(M2(kappa)) = the minimum value of ord(M3(kappa)), and lies strictly
between o(Z_2) and o(VB\P + Sigma-1 induction). The maximum value of
ord(M1(kappa)) lies strictly between o(type theory) and o(Z). Assuming that
there is a cardinal that is simultaneously n-Mahlo for all n >= 1, the
maximum value of ord(M2(kappa)) lies strictly between o(ZFC + {there exists
an n-Mahlo cardinal}_n) and o(ZFC + (there exists a cardinal that is
simultaneously n-Mahlo for all n >= 1)). Assuming that there is a cardinal
that is simultaneously n-subtle for all n >= 1, the maximum value of
ord(M3(kappa)) lies strictly between o(ZFC + {there exists an n-subtle
cardinal}_n) and o(ZFC + (there exists a cardinal that is simultaneously
n-subtle for all n >= 1)).

THEOREM 2.3. The three min's in Theorem 2.2 are realized at and only at
kappa = omega_1. The first max in Theorem 2.2 is realized at any kappa >=
omega_omega. The second max in Theorem 2.2 is realized at any kappa that is
simultaneously n-Mahlo for all n >= 1. The third max in Theorem 2.2 is
realized at any kappa that is simultaneously n-subtle for all n >= 1.

PROBLEM: What are ord(M1(kappa)), ord(M2(kappa)), ord(M3(kappa)), for
infinite cardinals kappa? We conjecture that the problem can be completely
resolved in ZFC + V=L. It seems as though Jensen's work on gap n two
cardinal theorems should be enough to answer some of these questions. We
will report on this later.

Note that we have not suceeded in getting a characterization of something
close to o(ZF); what we get is either a lot smaller or a lot bigger than o(ZF).

We can accomplish this by taking a different approach,
which is less set theoretic. Under this different approach, we obtain new
"structural" independence results which are of independent
interest. Hence we report on these developments in a separate posting,
"Structural independence results and provable ordinals."