[FOM] 234:Affine Pi01 Independence
Harvey Friedman
friedman at math.ohio-state.edu
Sat Nov 20 21:54:36 EST 2004
We now use restricted integral affine transformations. These are affine
transformations restricted to the solution set of a finite system of linear
inequalities, all with integer coefficients.
See Proposition 6.
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}. Let T:[r]^k into N, and 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 use U. for disjoint union.
We take min(emptyset) = max(emptyset) = 0.
We start with a fixed point theorm.
THEROEM 1. For all T:N^k into N, some A = T<[A^k]' containedin N. A is
unique, infinite, contains 0, and have a common element from {1,2}. Even if
k = 1, it is not possible to specify any number other than 0 in advance,
independently of T.
THEOREM 2. For all T:[r]^k into N, some A,T<[A^k]' contain the same elements
of rng(T).
We wish to consider common elements of A,T<[A^k]'.
THEOREM 3. For all T:[r]^k into N, some A,T<[A^k]' contain 0 and a common
element from {1,2}, and the same elements of rng(T). Even if k = 1, it is
not possible to specify any number other than 0 in advance, independently of
T,r.
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.
For E containedin N, let E! = {x!: x in E}. For x in N^s, we define x! =
(x_1!,...,x_s!).
We use cross section notation T_x, where x is a vector of any nonzero
length. Note that dom(T_x) depends on the length of x.
We take min(emptyset) = 0.
The following is an immediate weakening of Theorem 2.
THEOREM 4. For all T in RAF([p!]^k,[k]), some A,T<[A^k]' contain the same
min(T_x![A^<k)]).
The following is an immediate weakening of Theorem 3.
THEOREM 5. For all T in RAF([p!]^k,[k]), some A,T<[A^k]' contain 0 and a
common element from {1,2}, and the same min(T_x![A^<k)]).
In Theorem 5, Is it possible to specify a positive common element in
advance, depending only on k and not on T,p?
PROPOSITION 6. For all T in RAF([p!]^k,[k]), some A,T<[A^k]' contain (8k)!!
and the same min(T_x![A^<k]).
Proposition 6 is clearly Pi01. Here is an expanded version of Proposition 7,
which is in explicitly Pi01 form, and trivially equivalent to Proposition 6.
PROPOSITION 7. For all k,p >= 1 and T in RAF([p!]^k,[k]), there exists A
containedin [k^2 p!] such that (8k)!! in A\T<[A^k], and for all x in [p]^<k,
min(T_x![A^<k]) in A delta T<[A^k].
As things stabilize, we will sharpen the (8k)!!.
THEOREM 8. Theorem is provable in RCA and Theorems 2-5 are provable in EFA
(exponential function arithmetic). Propositions 6,7 are provably equivalent,
over ACA, to the consistency of MAH = ZFC + {there exists an n-Mahlo
cardinal}_n.
If we set p to be certain simple functions of k, rather than arbitrary, then
we can control the strength of Propositions 6,7 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.
*************************************
I use www.math.ohio-state.edu/~friedman/ for downloadable manuscripts.
This is the 234th 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
Harvey Friedman
More information about the FOM
mailing list