[FOM] 429: Finite Games and Incompleteness 2
Harvey Friedman
friedman at math.ohio-state.edu
Wed Jun 16 19:26:04 EDT 2010
THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION.
######################################################################
Here we use only strategies (not necessarily winning) for the given
relation game on a set A. These are functions f:A into A. We define
what we mean by "f is winning for B contained in A".
We specialize to the case of A = N^k. Thus strategies are f:N^k into
N^k. We define the p-span of f on B contained in N.
The remaining definitions are from
http://www.cs.nyu.edu/pipermail/fom/2010-June/014823.html
http://www.cs.nyu.edu/pipermail/fom/2010-June/014826.html
although we repeat the definitions here.
THEOREM. The following is false. Every downward relation game on N^k
has a winning strategy which is lower shift invariant over some
infinite set.
TEMPLATE. Every downward relation game on N^k has a strategy which is
winning on the k span of some infinite set over which the strategy is
well behaved.
TEMPLATE. Every downward relation game on N^k has a strategy which is
winning on the k span of some >= k element set over which the strategy
is well behaved.
TEMPLATE. Every order invariant downward relation game on N^k has a
strategy which is winning on the k span of some infinite set over
which the strategy is well behaved.
TEMPLATE. Every order invariant downward relation game on N^k has a
strategy which is winning on the k span of some >= k element set over
which the strategy is well behaved.
We also replace N with {0,...,t}, for t large relative to k, thereby
obtaining explicitly Pi01 forms.
We have also discovered that the relevant kind of well behavedness can
be stated in terms of equations involving min. This makes the
appropriate theory of well behavedness - which we have yet to work out
in good form - purely atomic. I.e., no quantifiers and no connectives.
The clearest way to state lower shift invariance still involves
implication, but it can be restated without implication - and for the
general theory of well behavedness, avoiding implication is preferable.
We will take up the theory of well behavedness of f:N^k into N^k on E
contained in N in later postings.
THIS POSTING IS SELF CONTAINED.
FINITE GAMES AND INCOMPLETENESS 2
by
Harvey M. Friedman
June 16, 2010
1. GAMES AND STRATEGIES.
2. SPANS AND LOWER SHIFT INVARIANCE.
3. INFINITE GAME THEOREM.
4. FINITE GAME THEOREMS.
5. ORDER INVARIANT GAME THEOREMS.
1. GAMES AND STRATEGIES.
A relation game G is a pair (A,R), where A is a set and R is contained
in A x A. We Let A be a set. We say that G is on A. A is referred to
as the domain of G.
Here are the rules of the game G = (A,R).
There are two players, Alice and Bob. First, the initial move x in A
is chosen by the referee. This is roughly analogous to Alice and Bob
playing chess starting with some referee chosen initial chess position
x, with Alice to move. Bobby Fischer proposed a chess tournament of
this rough kind related to randomnly permuting the back rows in the
usual initial position.
After the initial move x is chosen, play begins with Alice and Bob
alternately choosing elements of A. Alice moves first.
If a player makes the move z, and the preceding move is y, where not y
R z, then the game stops, and the player's opponent is declared the
winner.
This adjudication applies to Alice's first move - the preceding move
is the initial move x chosen by the referee.
In general, the play of G may last for infinitely many moves, reaching
no adjudication.
To avoid this situation, we say that G is a win/lose relation game if
and only if all plays of the game are of finite length.
We say that f is a strategy for the win/lose relation game G if and
only if f:A into A.
Let f be a strategy for G. It is clear what we mean by Alice (Bob)
following f. This means that all moves of Alice (Bob) are obtained by
applying f to the preceding move. In the case of Alice's first move,
the preceding move is the initial move chosen by the referee.
We say that f is a winning strategy for Alice (Bob) with initial move
x if and only if Alice (Bob) wins all plays of the game with initial
move x, as long as Alice (Bob) follows f.
We say that f is a winning strategy for G if and only if for all x in
A, f is a winning strategy for Alice with initial move x, or f is a
winning strategy for Bob with initial move x.
THEOREM 1.1. (Von Neumann). Every win/lose relation game has a winning
strategy.
Von Neumann did not state his theorem in quite this form, and he also
considered far more general games. Nevertheless, we can easily
obtained Theorem 1.1 from his results.
We now generalize the notion of winning strategy for win/lose relation
games.
Let B be contained in A. We say that f is a winning strategy for Alice
(Bob) on B with initial move x in B if and only if Alice (Bob) wins
all plays of the game with initial move x, as long as Alice (Bob)
follows f, and Bob (Alice) plays only moves from B.
We say that f is a winning strategy for G on B if and only if for all
x in B, f is a winning strategy for Alice on B with initial move x, or
f is a winning strategy for Bob on B with initial move x.
THEOREM 1.2. (Obvious). Every winning strategy for every win/lose
relation game is a winning strategy for the game on any subset of its
domain.
We say that G is a downward relation game on N^k if and only if G is a
game on N^k, where x G y implies max(x) > max(y). This obviously
implies that G is a win/lose game.
2. SPANS AND LOWER SHIFT INVARIANCE.
Let f:N^k into N^k and E be contained in N. The 0 span of E is E^k.
The r+1 span of E is the least V^k containing the r span of E and the
forward image of the r span of E under f.
We define the E shift as the map that sends x in E to the next largest
element of E. Obviously, the E shift is undefined at the largest
element of E. If E is infinite then the E shift maps E into E.
The E shift lifts naturally to E^k, by acting on coordinates.
We say that f is shift invariant over E if and only if E is contained
in N, and for all x,y in E^k, if y is the E shift of x, then f(x) =
f(y).
This notion is too strong for our purposes. We are interested in a
weakening of this notion that works well with many familiar
mathematical functions.
We say that f is lower shift invariant over E if and only if E is
contained in N, and for all x,y in E^k and 1 <= i <= k, if the E shift
of x is y and f_i(x) < min(x), then f_i(x) = f_i(y). Here f_i is the i-
th coordinate function of f.
There are some standard mathematical contexts where lower shift
invariance arises.
THEOREM 2.1. Every affine transformation T:N^k into N^k is lower shift
invariant over N. Every polynomial P;N^k into N^k with nonnegative
integer coefficients is lower shift invariant over N. Every piecewise
affine transformation T:N^k into N^k is lower shift invariant over
some infinite geometric progression. Every piecewise polynomial P:N^k
into N^k with nonnegative integer coefficients is lower shift
invariant over a tail of the double factorials.
In the theory of large cardinals, we have the following.
THEOREM 2.2. Let k >= 1. SRP proves that there exists lambda such that
every f:lambda^k into lambda^k is lower shift invariant over an
unbounded subset of lambda. SRP+ proves that for every k, there exists
lambda such that every f:lambda^k into lambda^k is lower shift
invariant over an unbounded subset of lambda. SRP and SRP+ are best
possible here over ZFC.
3. INFINITE GAME THEOREM.
PROPOSITION 3.1. Every downward relation game on N^k has a strategy
which is winning on the k span of some infinite set over which the
strategy is lower shift invariant.
THEOREM 3.2. Proposition 3.1 is provable in SRP+ but not from any
consequence of SRP that is consistent with RCA_0. Propositions 3.1 is
provably equivalent, over WKL_0, to Con(SRP).
Here SRP+ = ZFC + "for all k there exists a limit ordinal with the k-
SRP. SRP = ZFC + {there exists a limit ordinal with the k-SRP}_k. The
k-SRP asserts that every partition of the unordered k-tuples from
lambda into two pieces has a homogeneous set that is a stationary
subset of lambda.
4. FINITE GAME THEOREMS.
We write [t] for {0,1,...,t}. We write 2^[m], m >= 1, for the stack of
m 2's.
PROPOSITION 4.1. Every downward relation game on N^k has a strategy
which is winning on the k span of some >= k element set over which the
strategy is lower shift invariant.
PROPOSITION 4.2. Let t > 2^[8k]. Every downward relation game on [t]^k
has a strategy which is winning on the k span of some >= k element set
over which the strategy is lower shift invariant.
Note that Proposition 4.2 is explicitly Pi01.
THEOREM 4.3. Proposition 4.1, 4.2 are provable in SRP+ but not from
any consequence of SRP that is consistent with RCA_0. Propositions
4.1, 4.2 are provably equivalent, over RCA_0, to Con(SRP). In the case
of Proposition 4.2, SEFA suffices.
SEFA is super exponential function arithmetic.
5. ORDER INVARIANT GAME THEOREM.
We say that x,y in N^k 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 V contained in N^k is order invariant if and only if for
all order equivalent x,y in N^k, x in V iff y in V.
We say that a relation game G on N^k is order invariant if and only if
R is order invariant as a subset of N^2k.
PROPOSITION 5.1. Every downward order invariant relation game on N^k
has a strategy which is winning on the k span of some infinite set
over which the strategy is lower shift invariant.
PROPOSITION 5.2. Every downward order invariant relation game on N^k
has a strategy which is winning on the k span of some >= k element set
over which the strategy is lower shift invariant.
PROPOSITION 5.3. Every downward order invariant relation game on
[k(8k)!!]^k has a strategy which is winning on the k span of {(8k)!!,
2(8k)!!,...,k(8k)!!} over which the strategy is lower shift invariant.
Note that Proposition 5.3 is explicitly Pi01.
THEOREM 5.4. Proposition 5.1 - 5.3 are provable in SRP+ but not from
any consequence of SRP that is consistent with EFA. Propositions 5.1 -
5.3 are provably equivalent to Con(SRP) over RCA_0. For Proposition
5.1, we can use EFA.
EFA is exponential function arithmetic.
**********************
I use http://www.math.ohio-state.edu/~friedman/ for downloadable
manuscripts. This is the 429th 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 athttp://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 1graham
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
396: Free Reduction Theory 3 3/7/10 11:30PM
397: Free Reduction Theory 4 3/8/10 9:05AM
398: New Free Reduction Theory 1 3/10/10 5:26AM
399: New Free Reduction Theory 2 3/12/10 9:36AM
400: New Free Reduction Theory 3 3/14/10 11:55AM
401: New Free Reduction Theory 4 3/15/10 4:12PM
402: New Free Reduction Theory 5 3/19/10 12:59PM
403: Set Equation Tower Theory 1 3/22/10 2:45PM
404: Set Equation Tower Theory 2 3/24/10 11:18PM
405: Some Countable Model Theory 1 3/24/10 11:20PM
406: Set Equation Tower Theory 3 3/25/10 6:24PM
407: Kernel Tower Theory 1 3/31/10 12:02PM
408: Kernel tower Theory 2 4/1/10 6:46PM
409: Kernel Tower Theory 3 4/5/10 4:04PM
410: Kernel Function Theory 1 4/8/10 7:39PM
411: Free Generation Theory 1 4/13/10 2:55PM
412: Local Basis Construction Theory 1 4/17/10 11:23PM
413: Local Basis Construction Theory 2 4/20/10 1:51PM
414: Integer Decomposition Theory 4/23/10 12:45PM
415: Integer Decomposition Theory 2 4/24/10 3:49PM
416: Integer Decomposition Theory 3 4/26/10 7:04PM
417: Integer Decomposition Theory 4 4/28/10 6:25PM
418: Integer Decomposition Theory 5 4/29/10 4:08PM
419: Integer Decomposition Theory 6 5/4/10 10:39PM
420: Reduction Function Theory 1 5/17/10 2:53AM
421: Reduction Function Theory 2 5/19/10 12:00PM
422: Well Behaved Reduction Functions 1 5/23/10 4:12PM
423: Well Behaved Reduction Functions 2 5/27/10 3:01PM
424: Well Behaved Reduction Functions 3 5/29/10 8:06PM
425: Well Behaved Reduction Functions 4 5/31/10 5:05PM
426: Well Behaved Reduction Functions 5 6/2/10 12:43PM
427: Finite Games and Incompleteness 1 6/10/10 4:08PM
428: Typo Correction in #427 6/11/10 12:11AM
Harvey Friedman
More information about the FOM
mailing list