# [FOM] 432: Finite Games and Incompleteness 4

Harvey Friedman friedman at math.ohio-state.edu
Sat Jun 26 15:56:49 EDT 2010

```THIS RESEARCH WAS PARTIALLY SUPPORTED BY THE JOHN TEMPLETON FOUNDATION.

######################################################################

We no longer use strategies. We just use the winning and losing
positions of win/lose relation games - when restricted. Thus for each
such game, we consider the various win/lose pairs of sets, (A,B).

NOTE: Because of the well known relationship between win/lose relation
games and kernels in digraphs, we can view the game as a digraph, and
the win/lose pairs as "kernel pairs". This is the same thing, and is
explicit in the text.

We use a rather strong "inclusion relation" between (A,B), and (C,D),
where A,B,C,D are subsets of Q^k.

PROPOSITION. Every downward order invariant relation game on Q^k has 4
finite win/lose pairs forming a chain under strong inclusion.

The above statement is an independent explicitly Pi02 sentence, and
straightforward estimates make it an independent explicitly Pi01
sentence.

Intuitively speaking, an "inclusion relation" between (A,B) and (C,D),
where A,B,C,D are subsets of a space, asserts that

i. All objects built out of A in a certain way lie in C.
ii. All objects built out of A in a certain way lie in C union D.
iii. All objects built out of B in a certain way lie in D.
iv. All objects built out of B in a certain way lie in C union D.

Our particular notion of strong inclusion takes the space to be Q^k,
and fits nicely into i-iv. In fact, we can restrict ourselves to i,ii
only.

Although the notion of strong inclusion that we use is quite simple,
it is rather special. This situation BEGS for a general theory of
"inclusion relations" based on i-iv. We would expect to determine the
status of the Proposition above according to the choice of "inclusion
relation". An expected theorem also is that if we restrict to ii,iv,
or if we restrict to i,iii, then we do not get independence statements.

I am making progress on a such a general theory, based on the action
of affine transformations. This will be discussed in later postings.

THIS POSTING IS ENTIRELY SELF CONTAINED.

1. WIN/LOSE RELATION GAMES AND WIN/LOSE PAIRS.
2. DOWNWARD ORDER INVARIANT GAMES.
3. CUBES, UPPER SHIFT, AND STRONG INCLUSION.
4. INFINITE GAME THEOREM.
5. FINITE GMAE THEOREMS.

1. WIN/LOSE RELATION GAMES AND WIN/LOSE PAIRS.

Relation games are (given by) pairs (X,R), where R is contained in X x
X. Alice and Bob alternately play moves, which are elements of X.
Alice starts the game by playing any element of X. Subsequently, each
player must play some y such that x R y, where x is the last move
previously played by their opponent. If a player cannot make a legal
move, then that player loses, and their opponent wins.

Note that this is a zero memory game.

Such a game may never reach adjudication, since a play of the game of
infinite length is generally possible.

A win/lose relation game is a relation game such that there are no
plays of the game of infinite length. This is the same as saying that
there is no infinite walk in (X,R).

Let (X,R) be a win/lose game. A win/lose pair for (X,R) is a pair of
sets (A,B) such that

i. A is the set of winning moves in the game (X,R) where both players
are required to play in A union B.
ii. B is the set of losing moves in the game (X,R) where both players
are required to play in A union B.

Note that i,ii asserts that A (B) is the winning (losing) set in the
game (X,R)|(A union B).

The notion of winning move in this context is standard from game
theory. All moves are either winning or losing. Because these games
are zero memory, the moves themselves are inherently winning or
losing. I.e., the notion of winning/losing is player independent.

THEOREM 1.1. If (X,R) is a win/lose relation game then for any E
contained in X, there is a unique win/lose pair whose union is E.

We can relate this to kernels in digraphs as follows. Note that if
(X,R) is a relation game then (X,R) can also be viewed as a digraph
with vertex set X and edge set R.

THEOREM 1.2. Let (X,R) be a win/lose relation game. The win/lose pairs
for (X,R) are exactly the (A,B) such that A is the unique kernel of
the digraph (X,R)|(A union B), and B is the complement of the unique
kernel of the digraph (X,R)|(A union B). I.e., the win/lose pairs for
(X,R) are exactly the (kernel, complement of kernel) pairs in induced
subdigraphs of (X,R).

2. DOWNWARD ORDER INVARIANT GAMES.

We now focus on relation games (Q^k,R). We say that these games are on
Q^k.

We say that x,y in Q^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 A contained in Q^k is order invariant if and only if for
all order equivalent x,y in N^k, x in A iff y in A.

An order invariant relation game on Q^k is a relation game (Q^k,R),
where R is an order invariant subset of Q^2k.

3. CUBES, UPEPR SHIFT, AND STRONG INCLUSION.

Let A be a subset of Q^k. The cube of A is the least V^k containing A.

The upper shift of A is obtained by adding 1 to each nonnegative
coordinate of each element of A. E.g., the upper shift of {(-1,1,0),
(0,-2,4)} is {(-1,2,1),(1,-2,5)}.

Let A,B,C,D be subsets of Q^k. We define the relation

(A,B) is strongly included in (C,D)

as follows.

i. The cube of A and the zero vector are included in C union D.
ii. The upper shift of A is included in C.

In the interest of symmetry, we can strengthen this condition, without
changing our results.

iii. The cube of B and the zero vector are included in C union D.
iv. The upper shift of B is included in D.

Or, alternatively, we can use iii,iv only, again without changing our
results.

4. INFINITE GAME THEOREM.

PROPOSITION 4.1. Every downward order invariant game on Q^k has a win/
lose pair which is strongly included in itself.

THEOREM 4.2. Proposition 4.1 is provable in SRP+ but not from any
consequence of SRP that is consistent with RCA_0. Proposition 4.1, 3.2
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.

EFA is exponential function arithmetic.

5. FINITE GAME THEOREMS.

PROPOSITION 5.1. Every downward order invariant game on Q^k has four
(or r) win/lose pairs which form a chain under strong inclusion.

Note that Proposition 5.1 is explicitly Pi02.

The norm of (A,B), A,B contained in Q^k, is the maximum of the
magnitudes of the denominators and numerators in the reduced form of
the coordinates of the elements of A union B.

PROPOSITION 5.2. Every downward order invariant game on Q^k has four
(or r) win/lose pairs of norm at most (8k)!! (or (8kr)!!) which form a
chain under strong inclusion.

Note that Proposition 5.2 is explicitly Pi01.

Here (8k)!! and (8kr)!! are safe and convenient upper bounds, which
can be sharply reduced.

THEOREM 5.3. Propositions 5.1, 5.2 (all four forms) are provable in SRP+
but not from any consequence of SRP that is consistent with EFA.
Propositions 5.1, 5.2 (both forms) are provably equivalent, over EFA,
to Con(SRP).

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

manuscripts. This is the 432nd 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
429: Finite Games and Incompleteness 2  6/16/10  7:26PM
430: Finite Games and Incompleteness 3  6/18/10  6:14PM
431: Finite Incompleteness/Combinatorially Simplest  6/20/10  11:22PM
Harvey Friedman
```