FOM: 15:Structural Independence results and 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
14:New characterizations of the provable ordinals  4/8/98  2:09AM
14':Errata  4/8/98  9:48AM

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

Recall the definitions of logical equation and their solutions from "New
characterizations of the provable ordinals."

We now consider assertions of the following form: every logical equation
has a (countable) solution with an automorphism of a certain kind. Recall
that a solution is a triple (A,<,R), where R is a multivariate relation and
(A,<) is a linear ordering. Here automorphism means automorphism of (A,<,R).

We will consider only first order conditions on the automorphism. I.e., a
first order condition on (A,<,h), where h is an automorphism. Obviously, by
the downward Skolem Lowenheim theorem, the assertion is equivalent to the
assertion with "countable."

Also, clearly, every such assertion is provably equivalent to a pi-0-1
sentence.

THEOREM 1. The following is provable in RCA_0 + WKL. "Every logical
equation has a (countable) solution with an automorphism whose fixed points
form a proper initial segment" if and only if Con(PA).

THEOREM 2. The following is provable in RCA_0 + WKL. "Every logical
equation has a (countable) solution with a limit point and an automorphism
whose fixed points form a proper initial segment" if and only if Con(ZFC).

We can also consider embeddings h of (A,<,R) into itself. A critical point
of h is a point x such that h is the identity below x and h(x) > x.

THEOREM 3. The following is provable in RCA_0 + WKL. "Every logical
equation has a (countable) solution with an embedding that has a critical
point" is equivalent to Con(ZFC + {there exists a k-subtle cardinal}_k).

With this approach, we should be handle the entire large cardinal
hierarchy. We'll report on this later. But now we want to use this to
characterize the provable ordinals of ZF.

We follow the approach in "New characterizations of the provable ordinals,"
only we repeat the key definitions here in a little bit different notation
in order to make the ideas clearer.

A linearly ordered relation is a triple (A,<,R), where (A,<) is a linear
ordering and R is a muiltivariate relation on A. We say that (A,<) or
(A,<,R) is normal if and only if the natural numbers form an initial
segment of (A,<) under the usual ordering. The arity is the arity of R;
i.e., R is k-ary if and only if R containedin A^k. If R is k-ary, k >= 2,
and x in N^k-1, then we write R_x containedin N for the cross section {y:
R(x,y)}.

Let (A,<,R) be a normal k-ary linearly ordered relation. We define the
binary relation (A,<,R)* containedin N^k-1 x N^k-1 as follows.
(A,<,R)*(x,y) if and only if min(R^x) < min(R^y). Thus (A,<,R)*(x,y)
implies that min(R_x) and min(R_y) exist.

Let X be a nonempty class of normal linearly ordered k-ary relations, k >=
2. The core of X is the intersection of the (A,<,R)* for (A,<,R) in X.

The logical subclasses of X are those nonempty classes of X which are the
class of all solutions in X of some particular logical equation. Thus there
are countably many logical subclasses of X.

The logical cores of X are the cores of the logical subclasses of X.

Let X1 be the set of all normal linearly ordered relations with an
automorphism whose fixed points form a proper initial segment.
Let X2 be the set of all normal linearly ordered relations with a limit
point and an automorphism whose fixed points form a proper initial segment.

THEOREM 4. The logical cores of X1 are well founded and their ordinals are
exactly the ordinals < epilson_0. The logical cores of X2 are well founded
and their ordinals are exactly the provable ordinals of ZFC.

For the classes of normal linearly ordered relations considered in "New
characterizations of the provable ordinals," we also have that the logical
cores are well founded, and their ordinals are exactly the provable
ordinals of the theories cited there.