[FOM] 243:Inexplicit Pi01/Ordinals of Set Theories
Harvey Friedman
friedman at math.ohio-state.edu
Sun Dec 19 23:48:14 EST 2004
This posting concerns the problem of giving a mathematically natural
characterization of the proof theoretic ordinals of set theories.
We first give some new Pi01 independent statements. However, these
statements are not explicitly Pi01, as in posting 242. Here we rely on the
completeness theorem for predicate calculus to see that the statements are
equivalent to Pi01 statements.
As expected, these inexplicitly Pi01 statements are simpler than the
explicitly Pi01 statements of posting 242. Also: these do not have the
thematic character of BRT, with its classifications, and applicability to so
many mathematical contexts.
###############################################
1. INDEPENDENT INEXPLICITLY Pi01 STATEMENTS.
Let Q be the set of all rational numbers, with its usual linear ordering. We
say that R containedin Q^k is order invariant if and only if for all x,y in
Q^k, if x,y have the same order type then R(x) iff R(y).
Let R containedin Q^kp+k. An R-system is a pair (D,A), where
i) A containedin D^k containedin Q^k;
ii) A U. R[A^p] contains D^k.
(Note that there is a slight abuse of notation since we cannot read off k,p
from k+kp).
THEOREM 1. Let R containedin Q^kp+k be order invariant and D containedin Q
be well ordered. There is a unique R-system (D,A).
THEOREM 2. Every order invariant R containedin Q^kp+k has an R-system with a
nontrivial embedding.
PROPOSITION 3. Every order invariant R containedin Q^kp+k has an R-system
with an embedding with a critical point.
THEROEM 4. Theorem 1 is provably equivalent to ATR0 over RCA0. Theorem 2 is
provable in WKL0. Proposition 3 is provably equivalent, over WKL0, to the
consistency of ZFC + {there exists an n-subtle cardinal}_n.
We now take up some much stronger statements.
Let R containedin Q^kp+k. An R,<=-system is a pair (D,A), where
i) i) A containedin D^k containedin Q^k;
ii) A U. R[A^p] contains D^k<=.
Here D^k<= = {(x1,...,xk): x1,...,xk in D and x1 <= ... <= xk}.
Let j:D into D. We say that j is (D,A) amenable if and only if for all x in
D, j|<x is a cross section of A. Note that If A is k-dimensional then these
cross sections are given by fixing k-2 initial coordinates. Hence k >= 3 is
necessary.
PROPOSITION 5. For k >= 3, every order invariant R containedin Q^kp+k has an
R,<=-system with a nontrivial amenable embedding.
THEOREM 6. Proposition 5 is provably equivalent, over WKL0, to the
consistency of ZFC + {there exists an n-huge cardinal}_n.
We can certainly go further along these lines, at the cost of being a little
bit more complicated. I.e., getting lots of nontrivial elementary embeddings
from ranks into themselves.
R-systems are of interest in their own right, without any assumption
concerning the existence of embeddings. Their order types are interesting -
more precisely, the order types such that every R has an R-system of that
order type.
Furthermore, a series of natural conditions can be placed on R-systems that
correspond to ZFC and to lots of fragments of ZFC.
In fact, an R-system can be viewed as a set theoretic laboratory. There is
an appropriate definition of cardinal, regular cardinal, inaccessible
cardinal, etcetera.
I.e., set theory without set theoretic infrastructure.
We will take this up at a later time.
2. PROOF THEORETIC ORDINALS OF CERTAIN SET THEORIES.
We now use the above to treat the proof theoretic ordinals of certain set
theories.
The proof theoretic ordinal of a set theory is the sup of the ordinals alpha
such that there exists a presentation of a recursive ordering of order type
alpha for which the set theory proves that the ordering is a well ordering.
We write |T| for the proof theoretic ordinal of T.
We are now going to associate an ordering <R to every order invariant R
living in some Q^kp+k.
Let n,m in N. We define n >R m if and only if
for all R-systems (D,A) with an embedding with a critical point, the
greatest coordinate of the lexicographically n-th element of A is greater
than the greatest coordinate of the lexicographically m-th element of A.
Let SUB = ZFC + {there exists an n-subtle cardinal}_n. Let SUB+ = ZFC + "for
all n, there exists an n-subtle cardinal".
THEOREM 7. Each <R is a well founded r.e. relation. The sup of the ordinals
of the <R lies strictly between |SUB| and |SUB+|.
Let n,m in N. We define n >'R m if and only if
for all R,<=-systems (D,A) with a nontrivial amenable embedding, the
greatest coordinate of the lexicographically n-th element of A is greater
than the greatest coordinate of the lexicographically m-th element of A.
Let HUGE = VBC + {there exists an n-huge cardinal}_n. Let HUGE+ = VBC + "for
all n, there exists an n-huge cardinal".
THEOREM 8. Each <'R is a well founded r.e. relation. The sup of the ordinals
of the <'R lies strictly between |HUGE| and |HUGE+|.
NOTE: For all of these results, it suffices to use just one choice of rather
small integers k,p. I will later investigate just which k,p suffice.
*************************************
I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 243rd in a series of self contained numbered postings to
FOM covering a wide range of topics in f.o.m. The list of previous
numbered postings #1-149 can be found at
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html in the FOM
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:
150:Finite obstruction/statistics 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
154:Orderings on theories 5:28AM 6/25/02
155:A way out 8/13/02 6:56PM
156:Societies 8/13/02 6:56PM
157:Finite Societies 8/13/02 6:56PM
158:Sentential Reflection 3/31/03 12:17AM
159.Elemental Sentential Reflection 3/31/03 12:17AM
160.Similar Subclasses 3/31/03 12:17AM
161:Restrictions and Extensions 3/31/03 12:18AM
162:Two Quantifier Blocks 3/31/03 12:28PM
163:Ouch! 4/20/03 3:08AM
164:Foundations with (almost) no axioms 4/22/03 5:31PM
165:Incompleteness Reformulated 4/29/03 1:42PM
166:Clean Godel Incompleteness 5/6/03 11:06AM
167:Incompleteness Reformulated/More 5/6/03 11:57AM
168:Incompleteness Reformulated/Again 5/8/03 12:30PM
169:New PA Independence 5:11PM 8:35PM
170:New Borel Independence 5/18/03 11:53PM
171:Coordinate Free Borel Statements 5/22/03 2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals 5/34/03 1:55AM
173:Borel/DST/PD 5/25/03 2:11AM
174:Directly Honest Second Incompleteness 6/3/03 1:39PM
175:Maximal Principle/Hilbert's Program 6/8/03 11:59PM
176:Count Arithmetic 6/10/03 8:54AM
177:Strict Reverse Mathematics 1 6/10/03 8:27PM
178:Diophantine Shift Sequences 6/14/03 6:34PM
179:Polynomial Shift Sequences/Correction 6/15/03 2:24PM
180:Provable Functions of PA 6/16/03 12:42AM
181:Strict Reverse Mathematics 2:06/19/03 2:06AM
182:Ideas in Proof Checking 1 6/21/03 10:50PM
183:Ideas in Proof Checking 2 6/22/03 5:48PM
184:Ideas in Proof Checking 3 6/23/03 5:58PM
185:Ideas in Proof Checking 4 6/25/03 3:25AM
186:Grand Unification 1 7/2/03 10:39AM
187:Grand Unification 2 - saving human lives 7/2/03 10:39AM
188:Applications of Hilbert's 10-th 7/6/03 4:43AM
189:Some Model theoretic Pi-0-1 statements 9/25/03 11:04AM
190:Diagrammatic BRT 10/6/03 8:36PM
191:Boolean Roots 10/7/03 11:03 AM
192:Order Invariant Statement 10/27/03 10:05AM
193:Piecewise Linear Statement 11/2/03 4:42PM
194:PL Statement/clarification 11/2/03 8:10PM
195:The axiom of choice 11/3/03 1:11PM
196:Quantifier complexity in set theory 11/6/03 3:18AM
197:PL and primes 11/12/03 7:46AM
198:Strong Thematic Propositions 12/18/03 10:54AM
199:Radical Polynomial Behavior Theorems
200:Advances in Sentential Reflection 12/22/03 11:17PM
201:Algebraic Treatment of First Order Notions 1/11/04 11:26PM
202:Proof(?) of Church's Thesis 1/12/04 2:41PM
203:Proof(?) of Church's Thesis - Restatement 1/13/04 12:23AM
204:Finite Extrapolation 1/18/04 8:18AM
205:First Order Extremal Clauses 1/18/04 2:25PM
206:On foundations of special relativistic kinematics 1 1/21/04 5:50PM
207:On foundations of special relativistic kinematics 2 1/26/04 12:18AM
208:On foundations of special relativistic kinematics 3 1/26/04 12:19AAM
209:Faithful Representation in Set Theory with Atoms 1/31/04 7:18AM
210:Coding in Reverse Mathematics 1 2/2/04 12:47AM
211:Coding in Reverse Mathematics 2 2/4/04 10:52AM
212:On foundations of special relativistic kinematics 4 2/7/04 6:28PM
213:On foundations of special relativistic kinematics 5 2/8/04 9:33PM
214:On foundations of special relativistic kinematics 6 2/14/04 9:43AM
215:Special Relativity Corrections 2/24/04 8:13PM
216:New Pi01 statements 6/6/04 6:33PM
217:New new Pi01 statements 6/13/04 9:59PM
218:Unexpected Pi01 statements 6/13/04 9:40PM
219:Typos in Unexpected Pi01 statements 6/15/04 1:38AM
220:Brand New Corrected Pi01 Statements 9/18/04 4:32AM
221:Pi01 Statements/getting it right 10/7/04 5:56PM
222:Statements/getting it right again 10/9/04 1:32AM
223:Better Pi01 Independence 11/2/04 11:15AM
224:Prettier Pi01 Independence 11/7/04 8:11PM
225:Better Pi01 Independence 11/9/04 10:47AM
226:Nicer Pi01 Independence 11/10/04 10:43AM
227:Progress in Pi01 Independence 11/11/04 11:22PM
228:Further Progress in Pi01 Independence 11/12/04 2:49AM
229:More Progress in Pi01 Independence 11/13/04 10:41PM
230:Piecewise Linear Pi01 Independence 11/14/04 9:38PM
231:More Piecewise Linear Pi01 Independence 11/15/04 11:18PM
232:More Piecewise Linear Pi01 Independence/correction 11/16/04 8:57AM
233:Neatening Piecewise Linear Pi01 Independence 11/17/04 12:22AM
234:Affine Pi01 Independence 11/20/04 9:54PM
235:Neatening Affine Pi01 Independence 11/28/04 6:08PM
236:Pi01 Independence/Huge Cardinals 12/2/04 3:49PM
237:More Neatening Pi01 Affine Independence 12/6/04 12:56AM
238:Pi01 Independence/Large Large Cardinals/Correction 12/7/04 10:31PM
239:Pi01 Update 12/11/04 1:12PM
240:2nd Pi01 Update 12/13/04 2:49AM
241:3rd Pi01 Update 12/13/04 4:08AM
242:4th Pi01 Update 12/18/04 9:47PM
Harvey Friedman
More information about the FOM
mailing list