[FOM] 230:Piecewise Linear Pi01 Independence
Harvey Friedman
friedman at math.ohio-state.edu
Sun Nov 14 21:38:47 EST 2004
We are still waiting for this round to stabilize, before preparing a rough
sketch.
This approach with integral piecewise linear functions has some real
advantages:
1. Integral piecewise linear functions appear in far more mathematics then
order invariant relations, even though the latter are more "elementary".
2. A is now a set of nonnegative integers.
3. Instead of saying that a multidimensional A lies outside some particular
sphere, we can now say that A contains a certain nonnegative integer.
4. We do not need the lexicographic ordering.
5. We do not need the default that min of the empty set is 0.
6. In general, we have a more well motivated notion replacing A,p-minimal.
In fact, we do not need a separate definition, but can incorporate it in the
statement itself.
We will have to use factorials instead of powers of 2.
There is an additional layer of argument needed to show that this statement
follows from the Mahlo cardinals of finite order, coming from the fact that
we have to deal with addition, and not just <, and must get some reasonable
estimate on the integer used at the end of the statement - (8k)!!. Without
this additional argument, we only get a corresponding statement with >>,
which is Pi02 and not Pi01.
So there is a lot to check. But, in various forms, most of the ideas
involved have been swirling around in my head for some time.
These developments in no way, shape, or form obsolete BRT.
##########################################
Let N be the set of all nonnegative integers.
Let T:N^k into N. We say that T is strictly dominating if and only if for
all x in N^k, F(x) > max(x). We say that A is T-free if and only if A
containedin N and no element of A is the value of T at elements of A.
THEOREM 1. For all k >= 1 and strictly dominating T:N^k into N, there is a
T-free set A containing N\T[A^k]. I.e., A = T[A^k]'. Furthermore, A is
unique, contains the origin, and is infinite.
Let k,r >= 1 and a_1,...,a_p in Z. We write PLF(N^k;a_1,...,a_p) for the
piecewise linear functions F:N^k into N with nonzero coefficients among
0,a_1,...,a_p. These are the functions presented by an affine function on
each of finitely many pieces, where each piece is presented by a set of
linear inequalities, where the nonzero coefficients used throughout are
among a_1,...,a_p.
PROPOSITION 2. For all k,p >= 1 and strictly dominating T in
PLF(N^k;1,...,k), there is a finite T-free set A containing {min(F[A^k]): F
in PLF(N^k;1!,2!,...,p!)}\T[A^k] and (8k)!!.
Compare Proposition 2 with Theorem 1.
In fact, we can use any double factorial sufficiently large relative to k.
Other quantities can also be used.
Note that Proposition 2 is explicitly Pi02. We can write A containedin
[0,b]^k, where b = b(k,p) is an innocent function of k,p, without changing
Proposition 2, so that Proposition 4 becomes explicitly Pi01.
As things stabilize, we will give a reasonable expression for b = b(k,p),
better than double exponential. Also we will use an expression that is more
careful (i.e., lower) than (8k)!!.
THEOREM 3. Theorems 1 is provable in RCA0. Proposition 2 is provably
equivalent, over EFA, to the consistency of MAH = ZFC + {there exists an
n-Mahlo cardinal}_n. If we remove "and (8k)!!", then Proposition 2 becomes
provable in RCA0, as it becomes a trivial consequence of Theorem 1.
There are certain changes that can be made in Proposition 2 without changing
Theorem 3. For instance, we can use PLF(N^k;-k,...,k) or PLF(N^k;1) instead
of PLF(N^k;1,...,k). We can also introduce another parameter and use
PLF(N^k;-r,...,r) and the integer (8kr)!!.
If we set p to be certain simple functions of k, rather than arbitrary, then
we can control the strength of the statement 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 230th 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
Harvey Friedman
More information about the FOM
mailing list