[FOM] 356: Simplified HIGH SCHOOL and Mapping Theorem
Harvey Friedman
friedman at math.ohio-state.edu
Fri Aug 14 09:31:17 EDT 2009
It appears that I have been able to show independence even for one
variable (instead of k variables). There is a cost: I have to work
with both sums and products of pairs. But this seems well worth this
minor cost. It may be possible to do this reduction to one variable
with just addition. However, it looks like I will not be able to claim
this result before writing the detailed paper on the function game.
1. UNARY HIGH SCHOOL FUNCTION GAME
Let f:Z+ into Z+. We define a solitaire game with r rounds. Each
round results in a subset of Z+. The set resulting from a round is a
subset of the set resulting from the succeeding rounds.
The game is considered won if and only if no element of the final set
is the value of f at k strictly smaller elements of the final set.
At the first round, any subset of Z+ can be played. However, generally
speaking, you must be very careful about which set you choose as your
first round of play.
Let X be the set resulting from round i, 1 <= i < k. At round i+1,
(possibly) new integers are thrown into X by a specific
nondeterministic process.
The player first enumerates the sums and products of pairs from X in
numerical order The exact order is not really important. We use the
strict numerical order for naturalness and specificity. We allow both
coordinates in pairs to be the same. These are the CANDIDATES for
insertion into the set. For each successive candidate, n, the player
either throws n into the set, or instead writes n = f(m), m < n, and
throws m into the set. It may be the case that numbers thrown into the
set here are already in the set.
THEOREM 1.1. For all f:Z+^k into Z and r >= 1, the unary function game
can be won using some infinite first round play. In fact, we can win
the game in such a way that all rounds of play result in the same
infinite set.
PROPOSITION 1.2. Let f:Z+ into Z+ and r >= 1, The unary function game
can be won, with r rounds, even if we require that the first round of
play be an infinite set of odd integers.
What are the possible first rounds of play, given f:Z+ into Z+, that
lead to a win? This is not clear. However, we offer the following
result.
PROPOSITION 1.3. Let f:Z+ into Z+, E be an infinite subset of Z+, and
r >= 1. The unary function game can be won, with r rounds, even if we
require that the first round play be an infinite subset of E.
Here is a version where the first round of play is finite. It
immediately follows that all subsequent rounds of play are finite.
PROPOSITION 1.4. Let f:Z+ into Z+, E be an infinite subset of Z+, and
p,r >= 1. The unary function game can be won, with r rounds, even if
we require that the first round play be a subset of E with at least p
elements.
THEOREM 1.5. Theorem 1.1 can be proved in RCA_0. Propositions 2-4 are
provable in SMAH+ but not in any consistent subsystem of SMAH.
Proposition 1.2 is provably equivalent to 1-Con(SMAH), over ACA.
Propositions 3,4 are provably equivalent to Pi11 reflection on SMAH,
over ACA.
There is the question of how nice the functions f can be so that these
independence results hold. In the case of the multivariate function
game in the next section, the answer is the piecewise linear functions
from Z+^k into Z+. This result does not apply to one variable.
The piecewise linear functions f:Z^k into Z can be viewed as the
functions that can be written in 0,1,+,-,| |. Then we can then use the
|f| restricted to Z+^k.
Here, instead of 0,1,+,-,| |, we can use 0,1,+,-,x, and floor(sqrt|
x|). This defines a family of functions f:Z^k into Z. We can use the |
f| restricted to Z+, where k = 1. Call these *positive integral square
root functions*.
THEOREM 1.6. Theorem 5 holds even if we restrict to positive integral
square root functions f:Z+ into Z+. We can win the game by playing
rather concrete sets; e.g., piecewise +,x,exp sets. This results in
arithmetic independence results. In fact, we can play any interval
(finite or infinite) of factorials in the first round, as long as the
least of these factorials is sufficiently large relative to the given
piecewise linear function. This results in a Pi03 sentence provably
equivalent, over ACA, to 1-Con(SMAH).
There is a way to get good finite independent statements without
restricting the class of functions, and looking only on initial
segments of integers. This involves some simple *counting*. We will
take this matter up later in its own section - FINITE COUNTING
STATEMENTS. See section 4 below.
2. MULTIVARIATE HIGH SCHOOL FUNCTION GAME
Let f:Z+^k into Z+. We define a solitaire game with r rounds. Each
round results in a subset of Z+. The set resulting from a round is a
subset of the set resulting from the succeeding rounds.
The game is considered won if and only if no element of the final set
is the value of f at k strictly smaller elements of the final set.
At the first round, any subset of Z+ can be played.
Let X be the set resulting from round i, 1 <= i < k. At round i+1,
(possibly) new integers are thrown into X by a specific
nondeterministic process.
The player first enumerates the sums and products of pairs from X in
numerical order (although this is natural but not really important).
We allow both coordinates in pairs to be the same. These are the
candidates for insertion into the set. For each successive candidate
n, the player either throws n into the set, or instead writes n =
f(m_1,...,m_k), m_1,...,m_k < n, and throws m_1,...,m_k into the set.
It may be the case that numbers thrown into the set here are already
in the set.
THEOREM 2.1. For all f:Z+^k into Z and r >= 1, the multivariate
function game can be won using some infinite first round play. In
fact, we can win the game in such a way that all rounds of play result
in the same infinite set.
PROPOSITION 2.2. Let f:Z+^k into Z+ and r >= 1, The multivariate
function game can be won, with r rounds, even if we require that the
first round of play be an infinite set of odd integers.
What are the possible first rounds of play, given f:Z+ into Z+, that
lead to a win? This is not clear. However, we offer the following
result.
PROPOSITION 2.3. Let f:Z+^k into Z+, E be an infinite subset of Z+,
and r >= 1. The multivariate function game can be won, with r rounds,
even if we require that the first round play be an infinite subset of E.
Here is a version where the first round of play is finite. It
immediately follows that all subsequent rounds of play are finite.
PROPOSITION 2.4. Let f:Z+ into Z+, E be an infinite subset of Z+, and
p,r >= 1. The multivariate function game can be won, with r rounds,
even if we require that the first round play be a subset of E with at
least p elements.
THEOREM 2.5. Theorem 2.1 can be proved in RCA_0. Propositions 2.2-2.4
are provable in SMAH+ but not in any consistent subsystem of SMAH.
Proposition 2.2 is provably equivalent to 1-Con(SMAH), over ACA.
Propositions 2.3,2.4 are provably equivalent to Pi11 reflection on
SMAH, over ACA.
There is the question of how nice the functions f can be so that these
independence results hold. We can use the piecewise linear functions
from Z+^k into Z+.
THEOREM 2.6. Theorem 5 holds even if we restrict to piecewise linear
functions f:Z+ into Z+. We can win the game by playing rather concrete
sets; e.g., piecewise +,x,exp sets. This results in arithmetic
independence results. In fact, we can play any interval (finite or
infinite) of factorials in the first round, as long as the least of
these factorials is sufficiently large relative to the given piecewise
linear function. This results in a Pi03 sentence provably equivalent,
over ACA, to 1-Con(SMAH).
3. POLYNOMIAL HIGH SCHOOL GAME
The idea here is to use only one polynomial, rather than two.
Let P:Z^k into Z be a polynomial. We define a solitaire game with k
rounds. Each round results in a subset of Z. The set resulting from a
round is a subset of the set resulting from the succeeding rounds. The
game is considered won if and only if no element n of the final set
can be written as P(m_1,...,m_k), where m_1,...,m_k is in the final
set, and 0 <= m_1,...,m_k < n/2.
At the first round, any subset of Z can be played.
Let X be the set resulting from round i, 1 <= i < k. At round i+1,
(possibly) new integers are thrown into X by a specific
nondeterministic process.
The player first enumerates the elements of P[X^k] in increasing
magnitude, with negatives before positives (although this is not
really important). These are the candidates for insertion into the
set. For each candidate n, the player either throws it into the set,
or instead writes n = P(m_1,...,m_k), 0 <= m_1,...,m_k < n/2, and
throws m_1,...,m_k into the set. It may be the case that numbers
thrown into the set here are already in the set.
This game can be won, even if we require that the first round play be
an infinite set of positive integers. However, it is necessary and
sufficient to use large cardinals to prove this fact. It is
equivalent, over ACA, to 1-Con(SMAH).
Let P be a polynomial. For all sufficiently large p,t, the game
can be won with first play {p!!,(p+1)!!,...,t!!}. However, it is
necessary and sufficient to use large cardinals to prove this fact. It
is equivalent, over ACA, to 1-Con(SMAH). This is an explicitly Pi03
independence result.
Here, if we take t to be a function of p, then we get explicitly Pi02
sentences corresponding to fragments of ZF (and higher). E.g., using
iterated exponentials of k goes through Russell's type theory with
infinity. The same phenomena appears using piecewise linear functions
in the unary and multivariate function games above.
4. COUNTING CONDITION
We place a counting condition on the plays in these games. Let 1 <=
p,r <= infinity. The "p,r counting condition" asserts that
i. The game has exactly r rounds of play.
ii. The first round of play consists of p positive integers.
iii. For all 1 <= i <= p, the number of integers played in the game,
of magnitude at most the i-th element of the first round play, is at
most (8ir)!.
For the purposes of this definition only, we allow p,r to be infinite.
This is the only place where we allow letters to stand for infinity.
Never again.
THEOREM 4.1. For all f:Z+ into Z+, the unary function game can be won
subject to the infinity,infinity counting condition. In fact, we can
win the game in such a way that all rounds of play are identical.
PROPOSITION 4.2. For all f:Z+ into Z+ and r >= 1, the unary function
game can be won subject to the infinity,r counting condition, where
all integers in the first play are odd.
PROPOSITION 4.3. For all f:Z+ into Z+ and p,r >= 1, the unary function
game can be won subject to the p,r counting condition, where all
integers in the first play are odd.
PROPOSITION 4.4. For all p,r there exists t such that the following
holds. For all f:[1,t] into [1,t], the unary function game can be won
subject to the p,r counting condition, where all integers in the first
play are odd elements of [1,t].
THEOREM 4.5. For all f:Z+^k into Z+, the multivariate function game
can be won subject to the infinity,infinity counting condition. In
fact, we can win the game in such a way that all rounds of play are
identical.
PROPOSITION 4.6. For all f:Z+^k into Z+ and r >= 1, the multivariate
function game can be won subject to the infinity,r counting condition,
where all integers in the first play are odd.
PROPOSITION 4.7. For all f:Z+^k into Z+ and p,r >= 1, the multivariate
function game can be won subject to the p,r counting condition, where
all integers in the first play are odd.
PROPOSITION 4.8. For all k,p,r there exists t such that the following
holds. For all f:[1,t]^k into [1,t], the multivariate function game
can be won subject to the p,r counting condition, where all integers
in the first play are odd elements of [1,t].
Note that Propositions 4.4, 4.8 are explicitly Pi02.
THEOREM 4.9. Theorems 4.1, 4.5 are provable in ACA. Propositions
4.2-4.4, 4.6-4.8, are provable in SMAH+ but not in any consistent
fragment of SMAH. They are provably equivalent, over ACA, to 1-
Con(SMAH).
We will discuss the High School Relation Games at a later time, which
lead to explicitly Pi01 independence results.
5. MAPPING THEOREM - EXPLICIT Pi01
Recall Propositions 2.1-2.3 and Theorem 2.4 in http://www.cs.nyu.edu/pipermail/fom/2009-August/013907.html
Also recall 3.1-3.3.
We have been able to eliminate the parameter p by replacing it with 2.
Also, we always need a subcube of (A-1 delta R<[A^2])^p, regardless of
p.
PROPOSITION 5.1. For all R contained in N^2k x N^k, some R intersect
A^3 inverts some infinite subcube of A to some subcube of (A-1 delta
R<[A^2])^2.
PROPOSITION 5.2. For all (unit coefficient) piecewise linear R
contained in N^2k x N^k, some R intersect A^3 inverts some infinite
subcube of A some subcube of (A-1 delta R<[A^2])^2. Furthermore, A and
its
aforementioned infinite subcube can be taken to be piecewise (base 2)
exponential.
PROPOSITION 5.3. For all unit coefficient piecewise linear R contained
in [0,t!]^2k x [0,t!]^k, some R intersect A^3 inverts some [16k,t]!
^k containedin A to some subcube of (A-1 delta R<[A^2])^2.
Note that Propositions 5.3,5.4 are explicitly Pi01.
THEOREM 5.4. Propositions 5.1-5.3 are provable in SMAH+ but not in any
consistent fragment of SMAH. Propositions 5.1-5.3 are provably
equivalent,
over ACA, to Con(SMAH).
We can also use regressive values as in http://www.cs.nyu.edu/pipermail/fom/2009-August/013907.html
PROPOSITION 5.5. For all R contained in N^2k x N^k, some R intersect
A^3 has finitely many regressive inverse values on some infinite
cube in N^k that it inverts to some subcube of (A delta R<[A^2])^2.
This supports another kind of explicitly Pi01 independent statement:
PROPOSITION 5.6. For all R contained in [0,!(8rk)]^2k, some R
intersect A^3 has at most (8k)! regressive inverse values on some
length r cube in [0,!(8rk)]^3 that it inverts to some subcube of (A
delta R<[A^2])^2.
THEOREM 5.7. Propositions SMT5,SMT6 is provable in SUB+ but not in any
consistent fragment of SUB. Propositions 5.5,5.6 are provably
equivalent, over ACA, to Con(SUB).
Here there are also natural ways to adjust parameters to get
explicitly Pi01 statements corresponding to the consistency of
fragments of ZF (and higher), as discussed at the end of section 3
above.
**********************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 356th 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-249 can be found at
http://www.cs.nyu.edu/pipermail/fom/2005-June/008999.html in the FOM
archives, 6/15/05, 9:18PM. NOTE: The title of #269 has been corrected
from the original.
250. Extreme Cardinals/Pi01 7/31/05 8:34PM
251. Embedding Axioms 8/1/05 10:40AM
252. Pi01 Revisited 10/25/05 10:35PM
253. Pi01 Progress 10/26/05 6:32AM
254. Pi01 Progress/more 11/10/05 4:37AM
255. Controlling Pi01 11/12 5:10PM
256. NAME:finite inclusion theory 11/21/05 2:34AM
257. FIT/more 11/22/05 5:34AM
258. Pi01/Simplification/Restatement 11/27/05 2:12AM
259. Pi01 pointer 11/30/05 10:36AM
260. Pi01/simplification 12/3/05 3:11PM
261. Pi01/nicer 12/5/05 2:26AM
262. Correction/Restatement 12/9/05 10:13AM
263. Pi01/digraphs 1 1/13/06 1:11AM
264. Pi01/digraphs 2 1/27/06 11:34AM
265. Pi01/digraphs 2/more 1/28/06 2:46PM
266. Pi01/digraphs/unifying 2/4/06 5:27AM
267. Pi01/digraphs/progress 2/8/06 2:44AM
268. Finite to Infinite 1 2/22/06 9:01AM
269. Pi01,Pi00/digraphs 2/25/06 3:09AM
270. Finite to Infinite/Restatement 2/25/06 8:25PM
271. Clarification of Smith Article 3/22/06 5:58PM
272. Sigma01/optimal 3/24/06 1:45PM
273: Sigma01/optimal/size 3/28/06 12:57PM
274: Subcubic Graph Numbers 4/1/06 11:23AM
275: Kruskal Theorem/Impredicativity 4/2/06 12:16PM
276: Higman/Kruskal/impredicativity 4/4/06 6:31AM
277: Strict Predicativity 4/5/06 1:58PM
278: Ultra/Strict/Predicativity/Higman 4/8/06 1:33AM
279: Subcubic graph numbers/restated 4/8/06 3:14AN
280: Generating large caridnals/self embedding axioms 5/2/06 4:55AM
281: Linear Self Embedding Axioms 5/5/06 2:32AM
282: Adventures in Pi01 Independence 5/7/06
283: A theory of indiscernibles 5/7/06 6:42PM
284: Godel's Second 5/9/06 10:02AM
285: Godel's Second/more 5/10/06 5:55PM
286: Godel's Second/still more 5/11/06 2:05PM
287: More Pi01 adventures 5/18/06 9:19AM
288: Discrete ordered rings and large cardinals 6/1/06 11:28AM
289: Integer Thresholds in FFF 6/6/06 10:23PM
290: Independently Free Minds/Collectively Random Agents 6/12/06
11:01AM
291: Independently Free Minds/Collectively Random Agents (more) 6/13/06
5:01PM
292: Concept Calculus 1 6/17/06 5:26PM
293: Concept Calculus 2 6/20/06 6:27PM
294: Concept Calculus 3 6/25/06 5:15PM
295: Concept Calculus 4 7/3/06 2:34AM
296: Order Calculus 7/7/06 12:13PM
297: Order Calculus/restatement 7/11/06 12:16PM
298: Concept Calculus 5 7/14/06 5:40AM
299: Order Calculus/simplification 7/23/06 7:38PM
300: Exotic Prefix Theory 9/14/06 7:11AM
301: Exotic Prefix Theory (correction) 9/14/06 6:09PM
302: PA Completeness 10/29/06 2:38AM
303: PA Completeness (restatement) 10/30/06 11:53AM
304: PA Completeness/strategy 11/4/06 10:57AM
305: Proofs of Godel's Second 12/21/06 11:31AM
306: Godel's Second/more 12/23/06 7:39PM
307: Formalized Consistency Problem Solved 1/14/07 6:24PM
308: Large Large Cardinals 7/05/07 5:01AM
309: Thematic PA Incompleteness 10/22/07 10:56AM
310: Thematic PA Incompleteness 2 11/6/07 5:31AM
311: Thematic PA Incompleteness 3 11/8/07 8:35AM
312: Pi01 Incompleteness 11/13/07 3:11PM
313: Pi01 Incompleteness 12/19/07 8:00AM
314: Pi01 Incompleteness/Digraphs 12/22/07 4:12AM
315: Pi01 Incompleteness/Digraphs/#2 1/16/08 7:32AM
316: Shift Theorems 1/24/08 12:36PM
317: Polynomials and PA 1/29/08 10:29PM
318: Polynomials and PA #2 2/4/08 12:07AM
319: Pi01 Incompleteness/Digraphs/#3 2/12/08 9:21PM
320: Pi01 Incompleteness/#4 2/13/08 5:32PM
321: Pi01 Incompleteness/forward imaging 2/19/08 5:09PM
322: Pi01 Incompleteness/forward imaging 2 3/10/08 11:09PM
323: Pi01 Incompleteness/point deletion 3/17/08 2:18PM
324: Existential Comprehension 4/10/08 10:16PM
325: Single Quantifier Comprehension 4/14/08 11:07AM
326: Progress in Pi01 Incompleteness 1 10/22/08 11:58PM
327: Finite Independence/update 1/16/09 7:39PM
328: Polynomial Independence 1 1/16/09 7:39PM
329: Finite Decidability/Templating 1/16/09 7:01PM
330: Templating Pi01/Polynomial 1/17/09 7:25PM
331: Corrected Pi01/Templating 1/20/09 8:50PM
332: Preferred Model 1/22/09 7:28PM
333: Single Quantifier Comprehension/more 1/26/09 4:32PM
334: Progress in Pi01 Incompleteness 2 4/3/09 11:26PM
335: Undecidability/Euclidean geometry 4/27/09 1:12PM
336: Undecidability/Euclidean geometry/2 4/29/09 1:43PM
337: Undecidability/Euclidean geometry/3 5/3/09 6:54PM
338: Undecidability/Euclidean geometry/4 5/5/09 6:38PM
339: Undecidability/Euclidean geometry/5 5/7/09 2:25PM
340: Thematic Pi01 Incompleteness 1 5/13/09 5:56PM
341: Thematic Pi01 Incompleteness 2 5/21/09 7:25PM
342: Thematic Pi01 Incompleteness 3 5/23/09 7:48PM
343: Goedel's Second Revisited 1 5/27/09 6:07AM
344: Goedel's Second Revisited 2 6/1/09 9:21PM
345: Thematic Pi01 Incompleteness 4 6/15/09 1:15PM
appears misnumbered as 344.
346: Goedel's Second Revisited 3 6/16/09 11:04PM
347: Goedel's Second Revisited 4 6/20/09 1:25AM
348: Goedel's Second Revisited 5 6/22/09 11:00AM
349: Pi01 Incompleteness/set series 7/20/09 11:21PM
350: one dimensional set series 7/23/09 12:11AM
351: Mapping Theorems/Mahlo/Subtle 8/6/09 10:59PM
352: Mapping Theorems/simpler 8/7/09 10:06PM
353: Function Generation 1 8/9/09 12:09PM
354: Mahlo Cardinals in HIGH SCHOOL 1 8/9/09 6:37PM
355: Mahlo Cardinals in HIGH SCHOOL 2 8/10/09 6:18PM
Harvey Friedman
More information about the FOM
mailing list