[FOM] 396: Free Reduction Theory 3

Sun Mar 7 23:20:50 EST 2010

#394, #395 represent the state of the art regarding the infinite  
statements, and the games. (The formulations for n-huge can be  
stretched to somewhat more than rank into itself). The game  
formulations for finite length already are Pi01 (using decision  
procedures) and easily lend themselves to clear estimates.

We have been thinking about better finite forms of the infinite  
statements. At least in the case of the SRP level statements, we have  
temporarily decided on the most straightforward way of going about  
this, which we now present.

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

We use Q for the set of all rational numbers.

Until we state Proposition 1.1, we fix subsets R,A,B of,
respectively, Q^2k, Q^k, Q^k.

We write x R y if and only if (x,y) in R. We say that y is a strict
reduction of x if and only if x,y are in Q^k,
max(x) > max(y), and x R y.

We say that y is a reduction of x if and only if y = x or y is a
strict reduction of x.

We say that B is a reduction of A if and only if every element of A  
has a reduction in B.

We say that A is free if and only if no element of A is a strict  
reduction of any element of A.

Q^k has a natural subspace structure. The subspaces are the sets E^k,  
where E is a set of rationals that includes 0. The cube of A is the  
least subspace including A.

The upper shift of x in Q^k is obtained by adding 1 to all nonnegative
coordinates. The upper shift of A is the set of all upper shifts of  
elements of A. We write ush(A) for the upper shift of A.

We say that x,y in Q^2k are order equivalent if and only if for all 1  
<= i,j <= k, x_i < x_j iff y_i < y_j.

We say that R is order invariant if and only if R is the union of  
equivalence classes under order equivalence.

THEOREM 1.1. In every order invariant R contained in Q^2k, every  
finite subset of Q^k has a finite reduction A such that A union ush(A)  
is free.

PROPOSITION 1.2. In every order invariant R contained in Q^2k, every  
finite subset of Q^k has a finite reduction A whose cube has a finite  
reduction B such that A union B union ush(B) is free.

PROPOSITION 1.3. In every order invariant R contained in Q^2k, every  
finite subset of Q^k has a finite reduction A whose cube has a finite  
reduction B whose cube has a finite reduction C such that A union B  
union C union ush(C) is free.

PROPOSITION 1.4. Let R be an order invariant subset of Q^2k, E be a  
finite subset of Q^k, and n >= 1. There exist free A_1 union ... union  
A_n union ush(A_1 union ... union A_n), where A_1 = E and each A_i+1  
is a reduction of the cube of A_i.

THEOREM 1.5. Propositions 1.3, 1.4 are provable in SRP+ but not in any  
consequence of SRP consistent with EFA. Propositions 1.3, 1.4 are  
provably equivalent to Con(SRP) over EFA.

Estimates on the size and numerators and denominators needed in  
Propositions 1.3, 1.4 are straightforward, thus obtaining explicitly  
Pi01 sentences.

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 396th 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-349 can be found at http://www.cs.nyu.edu/pipermail/fom/2009-August/014004.html
in the FOM archives.

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
356: Simplified HIGH SCHOOL and Mapping Theorem  8/14/09  9:31AM
357: HIGH SCHOOL Games/Update  8/20/09  10:42AM
358: clearer statements of HIGH SCHOOL Games  8/23/09  2:42AM
359: finite two person HIGH SCHOOL games  8/24/09  1:28PM
360: Finite Linear/Limited Memory Games  8/31/09  5:43PM
361: Finite Promise Games  9/2/09  7:04AM
362: Simplest Order Invariant Game  9/7/09  11:08AM
363: Greedy Function Games/Largest Cardinals 1
364: Anticipation Function Games/Largest Cardinals/Simplified 9/7/09
11:18AM
365: Free Reductions and Large Cardinals 1  9/24/09  1:06PM
366: Free Reductions and Large Cardinals/polished  9/28/09  2:19PM
367: Upper Shift Fixed Points and Large Cardinals  10/4/09  2:44PM
368: Upper Shift Fixed Point and Large Cardinals/correction  10/6/09
8:15PM
369. Fixed Points and Large Cardinals/restatement  10/29/09  2:23PM
370: Upper Shift Fixed Points, Sequences, Games, and Large Cardinals
11/19/09  12:14PM
371: Vector Reduction and Large Cardinals  11/21/09  1:34AM
372: Maximal Lower Chains, Vector Reduction, and Large Cardinals
11/26/09  5:05AM
373: Upper Shifts, Greedy Chains, Vector Reduction, and Large
Cardinals  12/7/09  9:17AM
374: Upper Shift Greedy Chain Games  12/12/09  5:56AM
375: Upper Shift Clique Games and Large Cardinals 1
376: The Upper Shift Greedy Clique Theorem, and Large Cardinals
12/24/09  2:23PM
377: The Polynomial Shift Theorem  12/25/09  2:39PM
378: Upper Shift Clique Sequences and Large Cardinals  12/25/09  2:41PM
379: Greedy Sets and Huge Cardinals 1
380: More Polynomial Shift Theorems  12/28/09  7:06AM
381: Trigonometric Shift Theorem  12/29/09  11:25AM
382: Upper Shift Greedy Cliques and Large Cardinals  12/30/09  2:51AM
383: Upper Shift Greedy Clique Sequences and Large Cardinals 1
12/30/09  3:25PM
384: THe Polynomial Shift Translation Theorem/CORRECTION  12/31/09
7:51PM
385: Shifts and Extreme Greedy Clique Sequences  1/1/10  7:35PM
386: Terrifically and Extremely Long Finite Sequences  1/1/10  7:35PM
387: Better Polynomial Shift Translation/typos  1/6/10  10:41PM
388: Goedel's Second Again/definitive?  1/7/10  11:06AM
389: Finite Games, Vector Reduction, and Large Cardinals 1  2/9/10
3:32PM
390: Finite Games, Vector Reduction, and Large Cardinals 2  2/14/09
10:27PM
391: Finite Games, Vector Reduction, and Large Cardinals 3  2/21/10
5:54AM
392: Finite Games, Vector Reduction, and Large Cardinals 4  2/22/10
9:15AM
393: Finite Games, Vector Reduction, and Large Cardinals 5  2/22/10
3:50AM
394: Free Reduction Theory 1  3/2/10  7:30PM
395: Free Reduction Theory 2  3/7/10  5:41PM

Harvey Friedman