[FOM] 226:Nicer Pi01 Independence

Wed Nov 10 10:43:44 EST 2004

In posting #225, there was a silly error in the definition of R<[E]. I wrote

R<[E] = {y in N^k: (therexists x in N^s)(R(x,y) and max(x) < max(y))}.

This should be 

R<[E] = {y in N^k: (therexists x in E)(R(x,y) and max(x) < max(y))}.

But note that throughout #225, I use two different notions of forward image.
R[E] and R<[E]. Here we consolidate these into a single notion of forward
image, R<[E]. With an eye towards some new ground to be broken in later
postings, we will use the notation R*E.

Here we also omit the versions in #225 that avoid the use of the important
parameter t.

For a quick glance, read Proposition 1.5.

NOTE: I continue to follow the strategy of letting this round of statements
settle down. This of course comes at the cost of making an error. Then I
will write a rough sketch and give a pointer to it. This round is not yet
played out. 

This development of course does not obsolete the BRT development in any way,
shape, or form. However, the explicitly Pi01 and Pi02 statements below are
substantially better than any explicitly Pi01 statements presently coming
out of the BRT development.

##############################################

1. ORDER INVARIANT RELATIONS AND Pi01 INDEPENDENT STATEMENTS.

Let N be the set of all nonnegative integers.

Let R containedin Ns+k and E containedin Nk. We use a particular notion of
forward image of R on E called the upper image of R on E. The ordinary image
of R on E is given by

RE = R[E^k] = {y: there exists x in E)(R(x,y))).

The upper image of R on E is given by

R*E = {y: (therexists x in E)(R(x,y) and max(x) < max(y))}.

We use U. for disjoint union.

The powers of n >= 1 are the numbers n^1,n^2,... .

All lower case letters represent arbitrary integers >= 1, unless indicated
otherwise.

THEOREM 1.1. Let R containedin N^2k. There exists a unique A
containedin N^k such that A U. R*A = N^k. A contains the origin.

It is easy to see that Theorem 1.1 is false (even just existence) if we use
the ordinary RA instead of R*A. E.g., take k = 1 and R(x,y) iff x = y.

Here is an obvious consequence of Theorem 1.1.

THEOREM 1.2. Let R_1,R_2,... containedin N^2k. There exist nonempty
A_1,A_2,... containedin N^k such that every nonempty R_i*A_j meets every A_p
U. R_p*A_p. 

Let q >= 0 and a_1,...,a_q >= 0. We say that R containedin N^s is order
invariant over a_1,...,a_q if and only if for all x,y in N^s, if
(x,a_1,...,a_q),(y,a_1,...,a_q) have the same order type then x in R iff y
in R. 

Let u >= 0. E without u is the set of all elements of E none of whose
coordinates are u.

PROPOSITION 1.3. Let R_1,R_2,... containedin N^2k each be order invariant
over some t powers of n, where n >> k,t. There exist nonempty A_1,A_2,...
containedin N^k such that every nonempty R_i*A_j meets every A_p U. R_p*A_p
without n-1.

For finite forms, we start by modifying Theorem 1.2.

THEOREM 1.4. Let R_1,...,R_m containedin N^2k. There exist nonempty finite
A_1,...,A_m containedin N^k such that every nonempty R_i*A_j meets every A_p
U. R_p*A_p.

PROPOSITION 1.5. Let R_1,...,R_m containedin N^2k each be order invariant
over some t powers of n, where n >> k,t. There exist nonempty finite
A_1,...,A_m containedin N^k such that every nonempty R_i*A_j meets every A_p
U. R_p*A_p without n-1.

The bounds in Propositions 1.3,1.5 are innocent:

PROPOSITION 1.3'. Let R_1,R_2,,... containedin N^2k each be order invariant
over some t powers of n, where n >> k,t. There exist nonempty A_1,A_2,...
containedin N^k such that every nonempty R_i*A_j meets every A_p U. R_p*A_p
without n-1. Furthermore, the >> can be given by a suitable double
exponential expression in k.

PROPOSITION 1.5'. Let R_1,...,R_m containedin N^2k each be order invariant
over some t powers of n, where n >> k,t. There exists nonempty finite
A_1,...,A_m containedin N^k such that every nonempty R_i*A_j meets every A_p
U. R_p*A_p without n-1. Furthermore, the >> can be given by a suitable
double exponential expression in k,t. In addition, the largest coordinate in
A can be bounded above by a suitable double exponential expression in k and
the largest power of n used in the hypothesis.

THEOREM 1.6. Propositions 1.3,1.5,1.3',1.5' are each provably equivalent,
over RCA0, to the consistency of MAH = ZFC + {there exists an n-Mahlo
cardinal}_n. If we remove "without n-1" then they become provable in RCA0.
In the case of Propositions 1.5,1.5', we can use EFA instead of RCA0.

THEOREM 1.7. The level of Mahloness needed to prove in Propositions
1.3,1.5,1.3',1.5' is roughly t.

There are other interesting ways to control the strength of these
Propositions. Instead of fixing t, we can set m to be simple functions of n.
This should allow us to get roughly Zermelo set theory and various fragments
thereof. In fact, there should emerge a nice correspondence between
numerical functions and consistency strengths of set theories, presumably
going all the way from fragments of finite set theory = PA up through ZFC
and various fragments, up through levels of the Mahlo cardinal hierarchy.

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

I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 226th 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

Harvey Friedman