# [FOM] 235:Neatening Affine Pi01 Independence

Harvey Friedman friedman at math.ohio-state.edu
Sun Nov 28 18:08:05 EST 2004

```In this posting, we make some minor changes that improve the flow of the
statement. See Propositions 4,5.

It appears that this round is very close to stabilizing, at which time I
will roll up my sleeves and check everything in detail, and provide a rough
sketch.

These developments in no way, shape, or form obsolete BRT.

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

Let N be the set of all nonnegative integers. For A containedin N and k >=
1, let A^k be the set of all k-tuples from A. Let A^<k be the set of all
tuples from A of nonzero length < k.

For r >= 0, let [r] = {0,...,r}. We say that A,B disagree at z if and only
if A,B are sets and z in A iff z notin B.

Let T:B^k into N, and B,E containedin N^k. We define the upper image of T on
E by

T<[E] = {T(x): x in E and T(x) > max(x)}.

We start with a fixed point theorem.

THEOREM 1. For all T:N^k into N, some A containedin N disagrees with T<[A^k]
at all elements of N.

Theorem 1 has the following obvious finite form.

THEOREM 2. For all T:[p]^k into N, some A containedin [p] disagrees with
T<[A^k] at all elements of [p].

It is easy to see that 0 must lie in A. We can study requirements concerning
membership of positive integers in A.

THEROEM 3. For all T:[p]^k into N, some A containedin [p] including 1 or 2
disagrees with T<[A^k] at all elements of [p].

We note that in Theorem 1, even if k = 1, it is not possible to specify any
positive integer in advance to be included in A, depending only on p.

However, the situation changes if we use rather well behaved T and weaken
"at all elements of N" to integers that are in some sense "generated" by
T,A, and the factorials.

Let k,r >= 1 and E containedin [r]. We write RAF([r]^k,E) for the set of all
restricted affine transformations T:[r]^k into N over E. These are the
affine transformations T:[r]^k into N restricted to the solution set of a
system of linear inequalities, where all coefficients used in the
transformation and the system are from E.

We use cross section notation T_x, where x is a vector of any nonzero finite
length. Note that dom(T_x) depends on the length of x. If x is too long,
then obviously dom(T_x) = emptyset.

We take min(emptyset) = 0. For x in N^s, we define x! = (x_1!,...,x_s!).

PROPOSITION 4. For all T in RAF([p]^k,[k]), some finite A containedin N
including (8k)!! disagrees with T<[A^k] at all min(T_x![A^<k]).

Proposition 4 is easily seen to be Pi01, since we can bound the A and x!.
With a bit of extra work, one can arrive at the following elegant explicitly
Pi01 form, which should be compared with Theorems 2 and 3.

PROPOSITION 5. For all T in RAF([p]^k,[k]), some A containedin [p] including
(8k)!! disagrees with T<[A^k] at all min(T_x![A^<k]) <= p.

As things stabilize, we will sharpen the (8k)!!.

THEOREM 6. Theorems 1-3 are provable in RCA0. Theorems 2,3 are provable in
EFA. Propositions 4,5 is provably equivalent, over ACA, to the consistency
of MAH = ZFC + {there exists an n-Mahlo cardinal}_n. If we remove
"containing (8k)!!" from Proposition 4 or 5, the resulting statement is
provable in EFA.

If we set p to be certain simple functions of k, rather than arbitrary, then
we can control the strength of Proposition 4 somewhat. We should be able
to get PA and n-th order arithmetic, for various n, as well as significant
fragments of ZFC, ZFC itself, and levels of the Mahlo hierarchy.

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

This is the 235th 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

Harvey Friedman

```