When medicine has invented a cure and you will
be able to see again, I will come to the hospital
with my laptop to show you
two girls one cup.

Again, I gave a talk for the best mathematics-club in the multiverse. This time, it is for "older" people, that is, pupils in their last year and young students. So I will try to keep this text short, assuming that the reader is able to find out some details, mostly from usual mathematical practice I know, himself. Also keep in mind that a large part of this text was created during hasty evenings when I had other things to do. If something is wrong or not clear, feel free to tell me.

I will use some results from Transfinite Chomp by S. Huddleston and J. Shurman which I found on this excellent post from Xor's hammer.

Also keep in mind this is not a scientific paper, I will not always put footnotes everywhere I use information from the named paper. Especially, I change the notation so it will (hopefully) be compatible with ZFC (that is, there is no set of ordinal Numbers, etc.), as I think I have seen proofs in that paper that are not correct because of this (but I might be mistaken).

1 Finite Chomp

Before understanding ordinal chomp, it is useful to know finite chomp, and what makes it so interesting. We will try to give a definition that is less "economic" than the usual ones, but much more compatible with the intuition of a chocolate bar, which is the usual metaphor for explaining chomp.

Keep in mind that these definitions are preliminary and will later be generalized.

Definition: As a slight abuse of notation, we identify every integer with the set of its preceding numbers. So 0=\emptyset, 1=\{0\}, 2=\{\emptyset,\{\emptyset\}\}=\{0,1\}, etc. - this will later fit into our definition of ordinal numbers. It has nice properties like a<b being equivalent to a\in b. For now, it just helps us to have a simpler notation of the functions involved.

Definition: A n\times m chocolate bar is a function n\times m\rightarrow 2. The function \mathfrak{I}_{nm}=\lambda_x1 is the initial chocolate bar. The function \mathfrak{F}_{nm}=\lambda_x0 is the final chocolate bar. We may leave out the indices if their value is clear from the context. A legal move on an n\times m chocolate bar f is some \mathfrak{m}=(x,y)\in f^{-1}(1). Its application f \xrightarrow{\mathfrak{m}} g defines a new chocolate bar g with gab = \left\{\begin{array}{cl}0 & \mbox{for } a\ge x\mbox{ and }b\ge y\\fab & \mbox{otherwise}\end{array}\right.. A chocolate bar f is called legal, if it is acquired by applying a sequence of legal moves to \mathfrak{I}, that is, if there exist (\mathfrak{m}_i)_{1\le i\le n} such that \mathfrak{I}\xrightarrow{\mathfrak{m}_1}\ldots\xrightarrow{\mathfrak{m}_n} f. It is a player 1 chocolate bar if 2\mathbb{Z}+n=2\mathbb{Z}, and a player 2 chocolate otherwise. A legal move is called player n move, if it is applied to a player n chocolate.

Lemma: Every sequence of legal moves is finite.
Proof: Trivially, the number of preimages of 1 decreases with every application, and the chocolate bar is finite.

Definition: Let \mathfrak{L}\subseteq (n\times m)^{<\omega} be the set of sequences of legal moves starting from \mathfrak{I}. These sequences form a tree of legal chocolate bars, where every edge connects a player 1 chocolate bar and a player 2 chocolate bar. A strategy for player n is a subtree in which
  • every branch of the tree ends in the final chocolate bar (that is, every branch is a whole game)
  • the final chocolate bar in every branch is a player n chocolate bar (that is, player n wins)
  • every player 3-n node in the subtree is adjacent to all the player n chocolate bars that are adjacent in the original tree (that is, the winning of player n does not depend on the choices of player 3-n

We distinguish between weak and strong existence and disjunction. Usually, this is done to get a finer distinction between constructive and non-constructive propositions. However, we do not want to get too deep into that topic. So we give an informal definition.

Informal Definition: The weak disjunction A\tilde{\vee}B between two propositions A and B is a disjunction which we proved without giving a possibility of deciding which one of these actually holds inside the proof. Strong disjunction A\vee B always comes with a theoretical possibility of decision directly inside the proof. The weak existence \tilde{\exists} holds if only the existence of an object is proved, but there is no way of calculating it giving imlicitly with the proof. With strong existence \exists comes such a way.

The distinction between those two kinds of existence and disjunction can be seen as one main difference between constructive and classical mathematics. While in constructive theories, one can set A\tilde{\vee}B := \lnot(\lnot A \wedge \lnot B), in non-constructive mathematics, this is equivalent to usual disjunction.


Lemma: For every m\in\mathbb{N}_2 there (strongly) exists a strategy \mathfrak{q} for player 1 from the quadratic board \mathfrak{I}_{mm}.
Proof: Player 1 has to use (1,1), and then answer every move (i,j) of the other player by (j,i). By a simple parity argument, it is easy to see that this enforces winning.

Lemma: For every chocolate bar b there either (weakly) exists a strategy for player 1, (weak-)or one for player 2.
Proof: Note first that the "or" is exclusive here: Assume both existed, then consider a strategy for player 1. It will have some edge from \mathfrak{I} to some player 2 chocolate bar from which winning is not possible for player 2 anymore. This contradicts the existence of a player 2 startegy.
On the other hand, assume there is no strategy for player 1 or player 2. Then there must be some move player 1 can make, such that player 2 still has no winning strategy after this move. Player 2 can answer with a move after which player 1 again has no winning strategy, and so on. This is a contradiction, as every game has finite length.

Theorem: For every m,n\in\mathbb{N}_2 there (weakly) exists a strategy \mathfrak{q} that wins against every other strategy from \mathfrak{I}_{mn}.
Proof: Assume player 2 had a strategy \mathfrak{r}. Then, since player 1 can make the first move (m-1,n-1), this strategy yields a player 1 strategy from the chocolate bar \lambda_{\vec{p}} (\vec{p}=(m-1,n-1))?0:I_{mn}\vec{p}. Let \vec{q} be the a first move of this strategy, especially, \vec{q}\le(m-1,n-1). This yields a player 2 strategy for \lambda_{\vec{p}} (\vec{p}\le\vec{q})?I_{mn}\vec{p}:0. But player 1 could also have chosen \vec{q} from the beginning, and would thus have a winning strategy. Contradiction, by the above Lemma.

So we have an explicit winning strategy for finite quadratic chocolate bars. Unfortunately, even though we know we can always win, we have no winning strategy except bruteforcing for the rest of the cases (except for some additional special cases like our above Lemma).

Short introduction to ordinal numbers

Definition: A (strict) well-ordering is a (strict) total ordering in which every set has a minimum. A transitive set is a set of which every element is also a subset. An ordinal (number) is a transitive set which is strictly well-ordered by the \in-Relation.

Here are some facts about ordinals which I will not prove:
  • The above notation n=\{m\mid m<n\} is consistent with them.
  • Every well-ordering on a set is isomorphic to some unique ordinal.
  • Every decreasing sequence of ordinals is finite.
  • The collection of ordinals \operatorname{On} forms a proper class. It is not a set.
  • Every ordinal x has a successor x\cup\{x\}.
  • Some ordinals also have a predecessor. If \alpha\neq 0 has no predecessor, we say that \alpha is a limit ordinal, writing \lim\alpha.
  • The smallest limit ordinal is called \omega, it is the set of finite (natural) numbers.

Definition: A cardinal \kappa is an ordinal which satisfies \kappa = \inf \{\alpha\in\operatorname{On}\mid \exists_f f : \alpha \rightarrow \kappa \mbox{ bijective}\}.

We will only need cardinals in one small argument, in which we just need some "upper bound" for stuff we want to do.

Transfinite Chomp

A transfinite chocolate bar is defined similarily to the finite ones: An \alpha\times\beta-chocolate bar is a function \alpha\times\beta\rightarrow 2, the initial chocolate bar is again \mathfrak{I}=\lambda_{x}1, and the final chocolate bar is again \mathfrak{F}=\lambda_{x}0. The definitions of legal moves and their applications are also similar: A legal move \mathfrak{m} on a chocolate bar f is a pair x\in\alpha\times\beta such that fx=1, and the application f\xrightarrow{\mathfrak{m}}g yields a chocolate bar gab = \left\{\begin{array}{cl}0 & \mbox{for } a\ge x\mbox{ 
and }b\ge y\\fab & \mbox{otherwise}\end{array}\right.. A chocolate bar is legal if it is the result of finitely many applications of legal moves from \mathfrak{I}.

We first prove a few generalizations for properties of finite chomp.

Lemma: The sequence (\mathfrak{m}_i)_i of moves is legal if and only if \forall_{i}\forall_{j<i} (\pi_1 \mathfrak{m}_i < \pi_1 \mathfrak{m_j} \vee \pi_2 \mathfrak{m}_i < \pi_2 \mathfrak{m_j}).
Proof: By definition of the application and \mathfrak{I}, f_i^{-1}(0)=\bigcup\limits_{j=1}^i \{ \mathfrak{p} \mid \pi_1\mathfrak{p} \ge \pi_1\mathfrak{m}_j \wedge \pi_2\mathfrak{p} \ge \pi_2\mathfrak{m}_j \}. Therefore, f_i^{-1}(1)=(\alpha\times\beta)\backslash f_i^{-1}(0) = \bigcap\limits_{j=1}^i \{ \mathfrak{p} \mid \pi_1\mathfrak{p} < \mathfrak{m}_j \vee \pi_2\mathfrak{p} < \mathfrak{m}_j \}, from which the Lemma follows directly.

Theorem: Every sequence (\mathfrak{m}_i)_i of legal moves is finite.
Proof: By the Lemma, we know that the sequences (\min\limits_{j\le i}\pi_1\mathfrak{m}_j)_i and (\min\limits_{j\le i}\pi_2\mathfrak{m}_j)_i are decreasing, with at least one of them strictly decreasing at every step. Therefore, the sequence (\max \{\min\limits_{j\le i}\pi_1\mathfrak{m}_j, \min\limits_{j\le i}\pi_2\mathfrak{m}_j\} + \min \{\min\limits_{j\le i}\pi_1\mathfrak{m}_j, \min\limits_{j\le i}\pi_2\mathfrak{m}_j\})_i strictly decreases and must hence be finite.

Lemma: For every chocolate bar b there either (weakly) exists a strategy for player 1, (weak-)or one for player 2.
Proof: The above proof only requires every game to be of finite length, so it also applies here.

Lemma: Player 1 has a winning strategy for \mathfrak{I}_{\alpha\alpha}, \alpha\in\operatorname{On}\backslash 2.
Proof: The strategy is the same as for the finite case, but we have no parity here. However, it is easy to see that after every player 2 move, player 1 recovers a quadratic state, from which he has a winning move again.

Theorem: If \alpha and \beta have predecessors, and not both are equal to 1, then player 1 has a winning strategy for \mathfrak{I}_{(\alpha+1)(\beta+1)}.
Proof: The argument is exactly the same as for the finite case.

One interesting part about transfinite chomp is that in some cases it is possible that the second player has a winning strategy.

Theorem: Let \beta\in\operatorname{On}\backslash\{0\}, and a legal chocolate bar f be given. Then there is a unique h\in\operatorname{On} such that player 2 wins \lambda_{\vec{p}} ((\mathfrak{I}_{bh}\vec{p})\cdot(f\vec{p})).
Proof: Firstly we show uniqueness. Assuming the existence of h_1\in h_2\in\operatorname{On} with the property, player 1 could use (0,h_1+1) to win, contradiction. We show the existence by induction on \beta. Parallely, we maintain an cardinal \kappa, such that all ordinals occuring are in \kappa (we have to do this to make sure everything we talk about is a set)
  • For \beta=1, we use induction on f^{-1}(1). If f^{-1}(1)=1\times 1, h=1, \kappa=1. Otherwise, we assume that for all legal chocolate bars (f_i)_{i\in I} with f_i^{-1}(1)\subseteq f^{-1}(1), there already exists a h_i with the property. Especially then, for all legal chocolate bars (f_i)_{i\in J\subseteq I} that can be reached from f by one move, there exist (h_i)_{i\in J}. Then h := \operatorname{mex} (h_i)_{i\in J} is the solution: Trivially, every move player 1 makes leads to a state which player 2 can now win. Notice that if \overline{\kappa} was our previous cardinal, \kappa = 2^{\overline{\kappa}} is sufficient for everything we do (I am too lazy now to reason why \kappa=\overline{\kappa}^+ should be sufficient).
  • For every other \beta, we may assume that for every pair of \beta'\in\beta and a legal chocolate bar f' some h(f',\beta') already exists. Let \kappa be the 2 to the power of the supremum of all previous cardinals. Furthermore, for every legal chocolate bar f' which can be reached from \lambda_{\vec{p}}.\mathfrak{I}_{\beta\gamma}\vec{p}\cdot f\vec{p} for some \gamma\in\kappa by a move \vec{q} with \pi_1\vec{q}\in\beta, we also already have a h(f,\beta,\gamma). Then the \operatorname{mex} of all these exists (since the cardinality is bounded), and its own cardinality is bounded, and it trivially satisfies what we want.
Corollary 1: The second player wins \alpha\times\omega if and only if \alpha=2.
Proof: For \alpha=1 this is trivial. For \alpha=2 trivially player 1 loses after every move not being of the form (1,x>0), so assume he chose such a move. Assuming there was no winning strategy for player 2 from this point is equivalent to assuming that there is no finite h>x, such that f with \mathfrak{I}_{2h}\xrightarrow{(1,x)}f can be won by player 1. But this contradicts the uniqueness of the previous theorem. For 2\in\alpha, player 1 may just choose (2,0) as first move and wins.