FOM: 154:Orderings on theories

Tue Jun 25 01:28:45 EDT 2002

1. ORDERINGS ON SET THEORIES.

By a set theory we will mean a theory in predicate calculus with equality and 
membership. 

Let S,T be two finitely axiomatized set theories. We define

S < T if and only if for every model M of T there is an element x of M such 
that ({y: y epilson_M x},epsilon_M) satisfies S.

Let T be a recursively axiomatized extension of ZF\P = ZF without power set.

The provable ordinal of T is the sup of the ordinals of the recursive well 
orderings which are given by an index for which it is provable in T that the 
index defines a recursive well ordering. 

THEOREM 1.1. Let T be a recursively  axiomatized extension of ZF\P with 
reflection, which has a well founded model. Then < on finitely axiomatized 
fragments of T is r.e. and well founded, with ordinal = the provable ordinal of 
T.

We can consider set theories axiomatizated by finitely many schemes. For such 
S,T, define 

S < T if and only if for every model M of T there is an element x of M such 
that according to M, ({y: y epilson_M x},epsilon_M) satisfies S.

THEOREM 1.2. Let T be a recursively axiomatized extension of ZF\P with 
reflection, which has a well founded model. Then < on the fragments of T given 
by finitely many schemes is well founded, with ordinal > the provable ordinal 
of T. The ordinal is a recursive ordinal. 

2. ORDERINGS ON FRAGMENTS OF Z_2.

There is a similar treatment for fragments of Z_2. We only state this for Z_2. 

Let S,T be finite fragments of Z_2, proving ACA_0. We define

S < T if and only if every model M of T has a second order object x such that 
according to M, x codes a beta model of S. 

THEOREM 2.1. < is r.e. and well founded, with ordinal = the provable ordinal of 
Z_2.

3. ORDERINGS ON SENTENCES IN LINEARLY ORDERED PREDICATE CALCULUS.

We use linearly ordered predicate calculus with one binary relation. All models 
are of the form (A,<,R), where A is a set, < is a strict linear ordering on A, 
and R is a binary relation on A. It will be convenient to allow A to be empty.

We say that (A,<,R) is an initial submodel of (B,<',S) if and only if 

i) (A,<,R) is a submodel of (B,<',S);
ii) for all x in A and y in B\A, x <' y.

We say that (B,<',S) is a single point extension of (A,<,R) if and only if (A,<
,R) is an initial submodel of (B,<',S) and B\A has cardinality 1. 

If two single point extensions of (A,<,R) are isomorphic by an isomorphism 
which is the identity on A, then we identify those extensions.

In a direct union of models, we take the union of a (possibly empty) set of 
models which is linearly ordered by initial submodelhood.  

We order the sentences in our language as follows. 

phi < psi if and only if every direct union of countable models of phi is 
countable and has a unique single point extension satisfying psi.

THEOREM 3.1. < is r.e. and well founded, and the ordinal of < is the provable 
ordinal of Z_2.

More generally, let kappa be an infinite cardinal.

phi <kappa psi if and only if every direct union of models of phi, each of 
cardinality < kappa, is of cardinality < kappa, and has a unique single point 
extension satisfying psi.

THEOREM 3.2. For all infinite cardinals kappa, <kappa is well founded and has 
recursive ordinal. Assuming large cardinals, there is a maximum ordinal among 
the <kappa, and it is the provable ordinal of MAH. In particular, if kappa is 
n-Mahlo for all n < omega, then the ordinal of <kappa is the provable ordinal 
of MAH.

Here MAH = ZFC + {there exists an n-Mahlo cardinal}_n.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.

This is the 154th in a series of self contained postings to FOM covering
a wide range of topics in f.o.m. Previous ones counting from #100 are:

100:Boolean Relation Theory IV corrected  3/21/01  11:29AM
101:Turing Degrees/1  4/2/01  3:32AM
102: Turing Degrees/2  4/8/01  5:20PM
103:Hilbert's Program for Consistency Proofs/1 4/11/01  11:10AM
104:Turing Degrees/3   4/12/01  3:19PM
105:Turing Degrees/4   4/26/01  7:44PM
106.Degenerative Cloning  5/4/01  10:57AM
107:Automated Proof Checking  5/25/01  4:32AM
108:Finite Boolean Relation Theory   9/18/01  12:20PM
109:Natural Nonrecursive Sets  9/26/01  4:41PM
110:Communicating Minds I  12/19/01  1:27PM
111:Communicating Minds II  12/22/01  8:28AM
112:Communicating MInds III   12/23/01  8:11PM
113:Coloring Integers  12/31/01  12:42PM
114:Borel Functions on HC  1/1/02  1:38PM
115:Aspects of Coloring Integers  1/3/02  10:02PM
116:Communicating Minds IV  1/4/02  2:02AM
117:Discrepancy Theory   1/6/02  12:53AM
118:Discrepancy Theory/2   1/20/02  1:31PM
119:Discrepancy Theory/3  1/22.02  5:27PM
120:Discrepancy Theory/4  1/26/02  1:33PM
121:Discrepancy Theory/4-revised  1/31/02  11:34AM
122:Communicating Minds IV-revised  1/31/02  2:48PM
123:Divisibility  2/2/02  10:57PM
124:Disjoint Unions  2/18/02  7:51AM
125:Disjoint Unions/First Classifications  3/1/02  6:19AM
126:Correction  3/9/02  2:10AM
127:Combinatorial conditions/BRT  3/11/02  3:34AM
128:Finite BRT/Collapsing Triples  3/11/02  3:34AM
129:Finite BRT/Improvements  3/20/02  12:48AM
130:Finite BRT/More  3/21/02  4:32AM
131:Finite BRT/More/Correction  3/21/02  5:39PM
132: Finite BRT/cleaner  3/25/02  12:08AM
133:BRT/polynomials/affine maps  3/25/02  12:08AM
134:BRT/summation/polynomials  3/26/02  7:26PM
135:BRT/A Delta fA/A U. fA  3/27/02  5:45PM
136:BRT/A Delta fA/A U. fA/nicer  3/28/02  1:47AM
137:BRT/A Delta fA/A U. fA/beautification  3/28/02  4:30PM
138:BRT/A Delta fA/A U. fA/more beautification  3/28/02  5:35PM
139:BRT/A Delta fA/A U. fA/better  3/28/02  10:07PM
140:BRT/A Delta fA/A U. fA/yet better  3/29/02  10:12PM
141:BRT/A Delta fA/A U. fA/grammatical improvement  3/29/02  10:43PM
142:BRT/A Delta fA/A U. fA/progress  3/30/02  8:47PM
143:BRT/A Delta fA/A U. fA/major overhaul  5/2/02  2:22PM
144: BRT/A Delta fA/A U. fA/finesse  4/3/02  4:29AM
145:BRT/A U. B U. TB/simplification/new chapter  4/4/02  4:01AM
146:Large large cardinals  4/18/02  4:30AM
147:Another Way  7:21AM  4/22/02
148:Finite forms by relativization  2:55AM  5/15/02
149:Bad Typo  1:59PM  5/15/02
150:Finite obstruction/statisics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02  
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02