FOM: 23:Q-Systems and Proof Theoretic Ordinals

[Harvey Friedman]

This is the 23rd 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

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

Here we treat set theory ranging from weak fragments of ZFC through ZFC
through large cardinals, in terms of linearly ordered model theory. We then
use this treatment to give model theoretic characterizations of the proof
theoretic ordinals of set theories. These characterizations are simpler and
clearer than those given in postings 14, 15, and 16.

I. Q-SYSTEMS AND SET THEORY

A Q-system is a triple (Q,<,R), where < is the usual ordering on the
rationals, Q, and R is a subset of Q^2.

We introduce some conditions on Q-systems. Here definability refers to
definability in (Q,<,R), and allows any parameters. <x-definability refers
to definability with parameters <x only. We use the cross sections R[y] =
{z in Q:R(y,z)}.

1. For all x in Q, every definable subset of (-infinity,x) is R[y], for
some y in Q.
2. Fix k >= 1. For all 0 <= x <= k, every definable subset of (-infinity,x)
is R[y], for some y < x+1.
3. For all x >= 0, every definable subset of (-infinity,x) is R[y], for
some y < x+1.
4. For all x >= 0, the range of every <x-definable function from
(-infinity,x) into Q is R[y], for some y < x+1.
5. Fix k >= 1. For all 0 <= x <= k, the range of every definable function
from (-infinity,x) into (-infinity,floor(x+1)) is R[y], for some y <
floor(x+1).
6. For all x >= 0, the range of every definable function from (-infinity,x)
into (-infinity,floor(x+1)) is R[y], for some y < floor(x+1).
7. For every definable A containedin Q^2 there exists x such that R[x] =
A[x] intersect (-infinity,x).
8. For every definable A containedin Q^2 there exists x < y such that R[x]
= A[x] intersect (-infinity,x) = A[y] intersect (-infinity,y).
9. For every definable A containedin Q^2 there exists positive integers n_1
< n_2 < ... such that for all i >= 1, R[n_i] = A[n_i] intersect
(-infinity,n_i) = A[n_i+1] intersect (-infinity,n_i).

There is an obvious strenghening of 9 involving A containedin Q^n which
gets us up into subtle cardinals of finite order. But in order to make a
really big jump, we introduce extended Q-systems. We say that (Q,<,R,j) is
an extended Q-system if and only if j is an elementary embedding from the
Q-system (Q,<,R) into itself.

We introduce some conditions on extended Q-systems. Here, definability
refers to definability in (Q,<,R,j).

10. For all x >= 0, every definable subset of (-infinity,x) is R_y, for
some y < j(x).
11. For all x >= 0, every definable subset of (-infinity,x) is R_y, for
some y < j(x) < floor(x+1).

To go further, we introduce 2-extended Q-systems. These are quintuples
(Q,<,R,j_1,j_2), where j_1 is an elementary embedding of (Q,<,R) into
itself, and j_2 is an elementary embedding of (Q,<,R,j_1) into itself.

12. For all x >= 0, every (Q,<,R) definable subset of (-infinity,x) is R_y,
for some y < j_1(x), and every (Q,<,R,j_1) definable subset of
(-infinity,x) is R_z for some z < j_2(x).

One can go further, but it would be overkill at this point.

Below, ZFC\P is ZFC without the power set axiom, and ZC is Zermelo set
theory with the axiom of choice. Also VBC is von Neumann Bernays class
theory with the axiom of choice for sets, and VB\R is VB without
replacement. WKL_0 is the 2nd system of reverse mathematics (the first is
RCA_0), based on Weak Konig's Lemma.

THEOREM 1.1. WKL_0 proves that there exists a Q-system satisfying 1 (with
complete diagram) if and only if Con(PA).

THEOREM 1.2. ACA. proves that there exists a Q-system satisfying 2 for k =
1 if and only if there exists a Q-system satisfying 5 for k = 1 if and only
if there exists a Q-system satisfying 7 if and only if Con(ZFC\P).

THEOREM 1.3. Fix k >= 1. ACA. proves that there exists a Q-system
satisfying 2 for k if and only if Con(ZFC\P + V(omega+k-1) exists).

THEOREM 1.4. ACA proves that there exists a Q-system satisfying 3 if and
only if Con(ZC).

THEOREM 1.5. ACA proves that there exists a Q-system satisfying 4 if and
only if Con(ZFC).

THEOREM 1.6. Fix k >= 2. ACA proves that there exists a Q-system satisfying
5 for k if and only if Con(ZFC\P + there exists k-1 strongly inaccessible
cardinals).

THEOREM 1.7. ACA proves that there exists a Q-system satisfying 6 if and
only if Con(ZC + there are infinitely many strongly inaccessible
cardinals).

THEOREM 1.8. ACA proves Con(ZFC + there exists a subtle cardinal) implies
there exists a Q-system satisfying 8 implies Con(ZFC + there exists
uncountably many weakly compact cardinals).

THEOREM 1.9. ACA proves Con(ZFC + there exists an almost ineffable
cardinal) implies there exists a Q-system satisfying 9 implies Con(ZFC +
there exists uncountably many subtle cardinals).

THEROEM 1.10. ACA proves that there exists an extended Q-system satisfying
10 if and only if Con(VB\R + there exists a nontrivial elementary embedding
of V into V). By results of Woodin, this implies Con(ZFC + there exists a
cardinal that is n-huge for all n >= 1).

THEOREM 1.11. ACA proves that there exists an extended Q-system satisfying
11 if and only if Con(VB\R + there exists an elementary embedding of V into
V which has infinitely many fixed points above its critical point). This
implies Con(ZF + for all n >= 1 there exists an elementary embedding of a
rank into a rank with at least n fixed points above its critical point).

THEOREM 1.12. ACA proves that there exists a 2-extended Q-system satisfying
12 if and only if Con(VB\R + there exists j_1,j_2 such that j_1 is a
nontrivial elementary embedding of V into V and j_2 is a nontrivial
elementary embedding of (V,j_1) into (V,j_1)). This implies, e.g., that
Con(VB + there exists a huge cardinal kappa and a nontrivial elementary
embedding from V(kappa) into V(kappa)).

We can replace ACA throughout by WKL_0 if we state the conditions in terms
of complete diagrams, as we did in Theorem 1.1.

We can also also state these results in terms of faithful interpretations.
There exists faithful interpretations between the class of (extended and
2-extended) Q-systems and the class of models of the associated formal
systems. In this formulation, ACA and WKL_0 would not appear.

II. PROOF THEORETIC ORDINALS

Let T be an adequate formal system, and consider all integers e >= 0 such
that T proves "e defines a recursive well ordering." The proof theoretic
ordinal of T is the strict sup of the order type of all recursive well
orderings defined by such e. The proof theoretic ordinal of T is itself a
recursive ordinal, and in some sense measures the strength of the system T.
We write this ordinal as ord(T).

Let M be any linearly ordered relational structure. We construct the
definability ordering of M, written DFO(M), as follows. DFO(M) is a quasi
ordering (i.e., reflexive and transitive), whose field is

the set of all formulas in the relational type of M with at most the free
variable x whose extension is an initial segment of M.

We define phi <= psi if and only if

the extension of phi is included in the extension of psi.

Let S be a nonempty set (or class) of linearly ordered relational
structures. We define DFO(S) to be the intersection of all DFO(M), M in S.
Note that DFO(S) is also a quasi ordering.

The ordinal of a quasi ordering <= is the least ordinal for which there is
a map h from the field of <= into that ordinal, where each h(x) is the
strict sup of the h(y) for which y < x.

The ordinal of a class of linearly ordered structures, S, is the ordinal of
DFO(S). This exists if and only if DFO(S) is well founded. We write this
ordinal as |S|.

For 1 <= i <= 9, let S_i be the set of all Q-systems obeying condition i.
For i = 10,11, let S_i be the set of all extended Q-systems obeying
condition i. Let S_12 be the set of all 2-extended Q-systems obeying
condition 12.

As you can see below, the ordinals of the S_i's overshoot the proof
theoretic ordinals of the corresponding formal systems somewhat.

However, we can naturally stratify the S_i's in order to get exact matches
in most cases. E.g., ord(ZFC\P) = ord(Z_2) is obtained by stratifying S_2
for k = 1 by stratifying the definable subset in condition 2 according to
its quantifier complexity, and taking the limit of the corresponding | |'s.
ord(ZC) is obtained by taking the limit over k of the |S_2 for k|. ord(ZFC)
is obtained by stratifying the definable function in condition S_4
according to its quantifier complexity, and taking the limit of the
corresponding | |'s. Etcetera.

THEOREM 2.1. epsilon_0 < |S_1| < epilson_epsilon_0.

THEOREM 2.2. ord(ZFC\P) < |S_2 for k = 1| = |S_5 for k = 1| = |S_7| <
ord(MKC\P).

THEOREM 2.3. ord(ZFC\P + V(omega_k-1) exists) < |S_5 for k| < ord(MKC/P +
V(omega_k-1) exists).

THEOREM 2.4. ord(ZC) < |S_3| < ord(MK\R).

THEOREM 2.5. ord(ZFC) < |S_4| < ord(MKC).

THEOREM 2.6. Let k >= 2. ord(ZFC\P + there exists at least k-1 strongly
inaccessible cardinals) <
|S_5 for k| < ord(MKC\P + there exists at least k-1 strongly inaccessible
cardinals).

THEOREM 2.7. ord(ZC + there exists infinitely many strongly inaccessible
cardinals) < |S_6| <
ord(ZF + there exists infinitely many strongly inaccessible cardinals).

THEOREM 2.8. ord(ZFC + there exists uncountably many weakly compact
cardinals) < |S_8| < ord(ZFC + there exists a subtle cardinal).

THEOREM 2.9. ord(ZFC + there exists uncountably many subtle cardinals) <
|S_9| < ord(ZFC + there exists an almost ineffable cardinal).

THEOREM 2.10. ord(ZFC + there exists a cardinal that is n-huge for all n >=
1) < ord(VB\R + there exists a nontrivial elementary embedding of V into V)
< |S_10| < ord(ZF + there exists a nontrivial elementary embedding of a
rank into a rank). The first inequality is by work of Woodin.

THEOREM 2.11. ord(ZF + for all n >= 1 there exists an elementary embedding
of a rank into a rank with at least n fixed points above its critical
point) < |S_11| < ord(VB\R + there exists an elementary embedding of V into
V which has infinitely many fixed points above its critical point).

THEOREM 2.12. ord(VB + there exists a huge cardinal kappa and a nontrivial
elementary embedding from V(kappa) into V(kappa)) < |S_12| < ord(VB\R +
there exists j_1,j_2 such that j_1 is a nontrivial elementary embedding of
V into V and j_2 is a nontrivial elementary embedding of (V,j_1) into
(V,j_1)).