[FOM] 371:Vector Reduction and Large Cardinals

[Harvey Friedman]

We present some more elegant finite games and finite sequences  
corresponding to the Stationary Ramsey Property hierarchy (intertwined  
with the Subtle Cardinal hierarchy). The presentation is self contained.

http://www.cs.nyu.edu/pipermail/fom/2009-November/014173.html is still  
in force.

VECTOR REDUCTION AND LARGE CARDINALS
by
Harvey M. Friedman
November 20, 2009

1. Terminology.
2. Vector Reduction Game.
3. Vector Reduction Sequences.

1. TERMINOLOGY.

Let Q be the set of all rationals.

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

We say that E contained in Q^k is order invariant iff for all order
equivalent x,y in Q^k, x in E iff y in E.

We say that R contained in Q^k x Q^k is order invariant iff R is order
invariant as a subset of Q^2k.

We say that R containedin Q^k x Q^k is a reduction iff R(x,y) implies  
max(y) < max(x).

The upper shift of x in Q^k is obtained by adding 1 to all of the
nonnegative coordinates, and leaving the negative coordinates fixed.  
We use us for the upper shift.

SRP+ = ZFC + "for all k there is a limit ordinal with the k-SRP". SRP  
= ZFC + {there is a limit ordinal with the k-SRP}_k. SRP = stationary  
Ramsey property.

2. THE VECTOR REDUCTION GAME G(R,us,n).

Let R be contained in Q^k x Q^k be a reduction, and n >= 1.

The game G(R,us,n) is played for n rounds. Alice and Bob alternately  
move, and make n moves each. Alice's moves are required to be elements  
of Q^k. Bob's moves (responses) are required to be two elements of Q^k  
- called the first and second parts of his move.

Alice is required to open the game with the zero vector in Q^k. Every  
subsequent move of Alice must be a length k subsequence of the  
sequence of all moves previously played by Bob. (Here subsequences  
must be forward, and can skip over terms).

Suppose Alice has just played x in Q^k. The first part of Bob's next  
move must be either x or an R reduction of x; i.e., some y such that y  
= x or R(x,y). The second part of Bob's next move must be the upper  
shift of the first part of Bob's next move.

If no two of Bob's moves are related by R, then Bob is declared the  
winner. Otherwise, Alice is declared the winner.

PROPOSITION 2.1. For every order invariant reduction R contained in  
Q^k x Q^k, Bob wins the vector reduction game G(R,us,k).

PROPOSITION 2.2. For every order invariant reduction R contained in  
Q^k x Q^k and n >= 1, Bob wins the vector reduction game G(R,us,n).

PROPOSITION 2.3. For every order invariant reduction R contained in  
Q^k x Q^k, Bob wins the vector reduction game G(R,us,infinity).

Note that these Propositions are not explicitly arithmetical. However,  
consider

PROPOSITION 2.4. For every order invariant reduction R contained in  
Q^k x Q^k, Bob wins the vector reduction game G(R,us,k), by playing  
only rationals whose numerators and denominators in reduced form have  
magnitude at most (8k)!.

PROPOSITION 2.5. For every order invariant reduction R contained in  
Q^k x Q^k and n >= 1, Bob wins the vector reduction game G(R,us,n), by  
playing only rationals whose numerators and denominators in reduced  
form have magnitude at most (8kn)!.

These two Propositions are explicitly Pi01.

THEOREM 2.6. Propositions 2.1 - 2.5 are provably equivalent to the
Upper Shift Fixed Point Theorem over WKL_0. They can be proved in SRP+  
but
not in any consistent fragment of SRP. They are provably equivalent,  
over RCA_0, to Con(SRP). Propositions 2.4, 2.5 are provably  
equivalent, over EFA, to Con(SRP)

3. VECTOR REDUCTION SEQUENCES.

Note that for each i >= 2, Alice's i-th move is determined by the  
choice of a length k subsequence of 1,2,3,...,2k(i-1). (There are 2k  
rationals in the plays made by Bob in each round).

So we can remove the game theoretic element in the following way. Let  
R contained

A k,n schedule tau consists of alpha_1,...,alpha_n, where each alpha_i  
is a length k subsequence of 1,2,...,2ik. Let R contained in Q^k x Q^k  
be a reduction, and n >= 1. An R,tau,us,n sequence is a sequence of  
the form x_1,...,x_2n from Q^k x Q^k such that the following holds.

i. x_1 is 0 or an R reduction of 0.
ii. x_2 = us(x_1).
iii. for 1 <= i <= n-1, x_2i+1 is y_i or an R reduction of y_i, where  
y_i is the subsequence of x_1,...,x_i given by alpha_i.
iv. for 1 <= i <= n-1, x_2i+2 = us(x_2i).

PROPOSITION 3.1. For every order invariant reduction R contained in  
Q^k x Q^k, and k,k schedule tau, there is an R,tau,us,k sequence no  
two terms of which are related by R.

PROPOSITION 3.2. For every order invariant reduction R contained in  
Q^k x Q^k, n >= 1, and k,n schedule tau, there is an R,tau,us,n  
sequence no two terms of which are related by R.

Note that these Propositions are explicitly Pi02. Now consider

PROPOSITION 3.3. For every order invariant reduction R contained in  
Q^k x Q^k, and k,k schedule tau, there is an R,tau,us,k sequence no  
two terms of which are related by R, where the numerators and  
denominators of the rationals that appear have magnitude at most (8k)!.

PROPOSITION 3.4. For every order invariant reduction R contained in  
Q^k x Q^k, and k,n schedule tau, there is an R,tau,us,n sequence no  
two terms of which are related by R, where the numerators and  
denominators of the rationals that appear have magnitude at most (8kn)!.

The latter two are explicitly Pi01.

THEOREM 3.5. Propositions 3.1 - 3.4 are provably equivalent to the
Upper Shift Fixed Point Theorem over WKL_0. They can be proved in SRP+  
but
not in any consistent fragment of SRP. They are provably equivalent,  
over RCA_0, to Con(SRP). Propositions 3.1 - 3.4 are provably  
equivalent, over EFA, to Con(SRP).

4. TEMPLATES.

The choice of the upper shift function can be conveniently abstracted
away.

Note that the upper shift if the obvious lifting of the one
dimensional upper shift from Q into Q to higher dimensions.

We let PPL(Q) be the family of partial f:Q into Q given by

a_1x + b_1 if x in I_1
...
a_nx + b_n if x in I_n

where n >= 1, the a's,b's are rationals, and the I's are pairwise
disjoint nonempty intervals with rational endpoints (or +-infinity).

In sections 2-3, we can use any finite list from PPL(Q) instead of
just the upper shift. Thus instead of setting an extra term to be the
upper shift of the previous term, we can reserve several terms, one
each for each function in the finite list from PPL(Q). Take care of
undefinedness using repeats.

The conjecture is that this leads to statements that are provable or
refutable in SUB+ - whereas some instances are neither provable nor
refutable in SUB (namely the ones using the upper shift). So,
according to this conjecture, large cardinals are sufficient to settle
all resulting questions, but ZFC is not sufficient.

If we use the shift f:Q into Q, where f(x) = x+1, then the statements
are refutable in RCA_0.

If we use the restricted upper shift f:Q into Q, where f(x) = x+1 if x  
= 0; undefined otherwise, then the statements are provable in ZFC.

9. EXERCISES.

There are two obvious kinds of exercises.

i. Make k very small, or make n very small. Then try to prove the
statements.
ii. Make k small, or even moderate, and write down some specific
strictly dominating order invariant R contained in Q^k x Q^k. These
can be presented by merely listing finitely many 2k tuples from
{1,...,2k}. Try to prove the statements for just R.

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

I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 371st 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
362: Simplest Order Invariant Game
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/20/09  12:14PM

Harvey Friedman