922: WQO Games

Mon Jan 10 05:32:47 EST 2022

PREFACE. There are now a lot of interesting finite games of a rather
recreational nature, with some serious mathematical theory. The
attraction centers around the specificity of the question: who has a
winning strategy? This is raised for very specific games. But at the
"serious" mathematical standpoint, these games don't have, or rarely
have, the air of being mathematically compelling, as games. Perhaps an
arguable candidate for most mathematically compelling, among these
recreational games, might be NIM formulated where we have a finite set
of positive integers, being successively reduced by the players in the
well known way, until it becomes empty. What you see below is a rather
principled set of specific games, of a clear mathematical nature, with
tremendous natural flexibility, and where we fundamentally ask who
wins, Alice or Bob? Aside from their genuine mathematical character,
can they actually be played? Well perhaps yes, it seems so, if you
look at the last section below about "bounded games". I think if the
parameters are in a sweet spot of size, computers will be able to play
perfectly, humans not having a clue. Turning that into a theorem
involving sizes of proofs is quite a challenge.

Let X = (X,<=) be a wqo. G(X) is the following two person game, Alice
and Bob as usual making alternating moves, Alice moving first.

On each player's turn, they play any x in X such that no previous
plays of either player is <= x.

A player loses when they can no longer make a play.

Because X is a wqo, this is a finite game in the sense that every game
history is finite.

For countable X, G(X) is a clopen game, and so ATR0 proves G(x) is
determined. Determinacy for clopen games is equivaelnt to ATR0 over
RCA0, and so presumably a similar argument should show that
determinacy for countable G(X) is equivalent to ATR0 over RCA0. See
Chapter 5 in Simpson's SOSOA book for this work due to Steel (he used
based theory RCA instead of RCA0).

QUESTION 1. How do we find out who wins, Alice or Bob, in G(X)?
Obviously, if X is simply an ordinal, or more generally, there is a
least element of X, then Alice wins easily by playing 0, or any least
element.

THE SUBSEQUENCE GAME

The mathematical interest in Question 1 depends of course on the
mathematical interest of the wqo X = (X,<=).

In the subsequence game, we let A be any fixed nonempty finite
alphabet. Then it is well known that the nonempty finite sequences
from A form a wqo under subsequence. So the associated game can be
spelled out clearly for the general mathematician as follows.

Alice and Bob play alternately with Alice starting the game. Each
player is required to play a nonempty finite sequence x from A such
that no previous play of either player is a subsequence. The first
time a player cannot make a play, the game ends and that player loses.

Who wins this game? If |A| = 1 then obviously Alice wins by playing
the sequence of length 1 (empty sequence not allowed by the rules). Of
course, if Alice plays anything else, then Bob wins by playing the
sequence of length 1.

Who wins this game if |A| = 2? And how do they win it? And for larger A?

More generally, but still intriguing, suppose we specify Alice's first
move to be a short sequence from A. Then who wins?

We can even specify the first few moves of the game. Then who wins?

Or we can merely demand that Alice start the game by a sequence of
specific small length, or a sequence of at least a specific small
length. Then who wins the game?

THE FINITE TREE GAME

We can use unlabeled finite rooted trees under inf preserving
embedding. Alice wins this game easily by playing just the root. We
can specify Alice's first move by a small finite rooted tree or put a
size requirement or structural requirement on Alice's first move. Then
who wins? For specificity, say, for example, that Alice's first move
is the root with 2 sons, or the root with 3 sons, say. Or Alice's
first move must have 4 vertices, or maybe at least 4 vertices.

NORMED GAMES; BOUNDED GAMES

Many wqo come with a natural norm which is a positive integer. In the
case of the subsequence game the norm is the length of the sequence.
In the case of the finite tree game, the norml is the number of
vertices.

Basic requirements can be placed on the norms of the successive plays.

For example, the bounded game requires that each player play an x in X
of norm at most one more than the norms of all previous plays by
either player. Instead of the +1 function here, we can require that
each play be at most f of the norm of all previous plays by either
player. Or we can put a bound on the plays according to the move
number.

If we do this kind of upper bounding, then we know, as in my finite
forms of Kruskal's theorem and finite wqo theory, that there is a
bound to the length of all plays of the game. So there is a number n
such that Alice or Bob wins the game in at most n moves. Getting
estimates on n for various versions of the game seems interesting.
Obviously a computer is going to be important here, but how can we use
serious combinatorial insights and computer algorithm theory to get
good bounds? The flexibility of these games is so enormous that this
promises to lead to a rather deep interaction between mathematician
and computers.

Instead of using the norm to put upper bounds on the size of the
plays, we can use the norm in another way - to put lower bounds on the
size of the plays. For instance, on the n-th move, the  player must
play with norm at least f(n), where f is a natural function like
identity, or +1, or doubling, or squaring, or exponentiating. Or, for
example, ,each play must have norm greater than the sum of the norms
of each previous play by either player. (This is also interesting with
"greater" replaced by "less than or equal to").

CONCLUSION

In each of these games, we know we have a winning strategy for one of
the two players. These games are very simple and natural
mathematically. Therefore we are compelled to find the winner, Alice
or Bob.

It seems unlikely but not impossible that some clever or powerful way
to look at all this would clarify the entire situation here.

Thus, it would appear that the entire GDP of the planet can easily be
burned up following all these natural research leads, including deep
interactions with computers.

However, I would not recommend that the entire GDP of the planet be
used for this purpose.

PS: Does Strategy Stealing have any role in these investigations?
https://en.wikipedia.org/wiki/Strategy-stealing_argument

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

My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 922nd 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-899 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/

900: Ultra Convergence/2  10/3/21 12:35AM
901: Remarks on Reverse Mathematics/6  10/4/21 5:55AM
902: Mathematical L and OD/RM  10/7/21  5:13AM
903: Foundations of Large Cardinals/1  10/12/21 12:58AM
904: Foundations of Large Cardinals/2  10/13/21 3:17PM
905: Foundations of Large Cardinals/3  10/13/21 3:17PM
906: Foundations of Large Cardinals/4  10/13/21  3:17PM
907: Base Theory Proposals for Third Order RM/1  10/13/21 10:22PM
908: Base Theory Proposals for Third Order RM/2  10/17/21 3:15PM
909: Base Theory Proposals for Third Order RM/3  10/17/21 3:25PM
910: Base Theory Proposals for Third Order RM/4  10/17/21 3:36PM
911: Ultra Convergence/3  1017/21  4:33PM
912: Base Theory Proposals for Third Order RM/5  10/18/21 7:22PM
913: Base Theory Proposals for Third Order RM/6  10/18/21 7:23PM
914: Base Theory Proposals for Third Order RM/7  10/20/21 12:39PM
915: Base Theory Proposals for Third Order RM/8  10/20/21 7:48PM
916: Tangible Incompleteness and Clique Construction/1  12/8/21   7:25PM
917: Proof Theory of Arithmetic/1  12/8/21  7:43PM
918: Tangible Incompleteness and Clique Construction/1  12/11/21  10:15PM
919: Proof Theory of Arithmetic/2  12/11/21  10:17PM
920: Polynomials and PA
921: Polynomials and PA/2

Harvey Friedman