2.2 The recursive order

Definition 2.4 Game comparison

✓

The relation \(x\preceq y\) is defined recursively by

\[ x\preceq y \quad \Longleftrightarrow \quad \bigl(\forall x^L\in X^L,\ \neg (y\preceq x^L)\bigr) \ \wedge \bigl(\forall y^R\in Y^R,\ \neg (y^R\preceq x)\bigr). \]

Strict comparison is

\[ x\prec y \quad \Longleftrightarrow \quad x\preceq y\ \wedge \ \neg (y\preceq x). \]

Definition 2.5 Game equivalence

✓

Two games \(x,y\in \mathcal{G}\) are equivalent, written \(x\sim y\), when each is weakly below the other:

\[ x\sim y \quad \Longleftrightarrow \quad x\preceq y\ \wedge \ y\preceq x. \]

This is the relation used later to identify games with the same game value. Equivalent games need not be literally equal as rooted trees or have identical option lists.

Definition 2.6 Well-founded induction schemes

✓

The development uses the following relations on one, two, three, and four games. For \(q=(q_1,q_2,q_3,q_4)\) and \(q'=(q'_1,q'_2,q'_3,q'_4)\), set

\[ \begin{aligned} y\mathrel R x & \quad \Longleftrightarrow \quad \operatorname {bd}(y){\lt}\operatorname {bd}(x),\\ (a’,b’)\mathrel B(a,b) & \quad \Longleftrightarrow \quad \operatorname {bd}(a’)+\operatorname {bd}(b’){\lt}\operatorname {bd}(a)+\operatorname {bd}(b),\\ (a’,b’,c’)\mathrel T(a,b,c) & \quad \Longleftrightarrow \quad \operatorname {bd}(a’)+\operatorname {bd}(b’)+\operatorname {bd}(c’){\lt}\operatorname {bd}(a)+\operatorname {bd}(b)+\operatorname {bd}(c),\\ q’\mathrel Qq & \quad \Longleftrightarrow \quad \sum _{i=1}^{4}\operatorname {bd}(q’_i){\lt}\sum _{i=1}^{4}\operatorname {bd}(q_i). \end{aligned} \]

Each relation is well founded because it is the inverse image of the well-founded order \({\lt}\) on \(\mathbb N\) under the corresponding sum-of-birthdays measure. They will be used for well-founded induction on one, two, three, and four games, respectively; replacing any coordinate by an option strictly decreases the relevant measure.

Theorem 2.7 Order calculus for games

✓

For all games \(x,a,b,c\), reflexivity and transitivity are the assertions

\[ x\preceq x, \qquad a\preceq b\ \wedge \ b\preceq c \quad \Longrightarrow \quad a\preceq c. \]

Consequently \(\sim \) is an equivalence relation, \(\prec \) is transitive, and strict and weak inequalities compose in either order.

Proof ▶

For reflexivity, use the one-game induction scheme of Definition 2.6. Suppose reflexivity is known for all games of birthday smaller than \(\operatorname {bd}(x)\), and unfold the comparison in Definition 2.4. If \(x^L\) is a left option and \(x\preceq x^L\), then the left-option clause of this last comparison says \(\neg (x^L\preceq x^L)\). On the other hand, Lemma 2.3 gives \(\operatorname {bd}(x^L){\lt}\operatorname {bd}(x)\), so the induction hypothesis gives \(x^L\preceq x^L\), a contradiction. If \(x^R\) is a right option and \(x^R\preceq x\), the right-option clause similarly says \(\neg (x^R\preceq x^R)\), again contradicting the induction hypothesis. Thus \(x\preceq x\).

For transitivity, use the three-game induction scheme of Definition 2.6. Assume \(a\preceq b\) and \(b\preceq c\), and induct on \(\operatorname {bd}(a)+\operatorname {bd}(b)+\operatorname {bd}(c)\). If \(a^L\) is a left option and \(c\preceq a^L\), then the induction hypothesis applied to the triple \((b,c,a^L)\) gives \(b\preceq a^L\). This contradicts the left-option clause of \(a\preceq b\) in Definition 2.4. Similarly, if \(c^R\) is a right option and \(c^R\preceq a\), the induction hypothesis for \((c^R,a,b)\) gives \(c^R\preceq b\), contradicting the right-option clause of \(b\preceq c\). Both recursive calls decrease because Lemma 2.3 replaces one coordinate by an option of smaller birthday. Hence \(a\preceq c\).

The remaining assertions follow directly from Definitions 2.4 and 2.5. Symmetry and transitivity of \(\sim \) are obtained by composing the two weak inequalities in the appropriate directions. For strict transitivity, compose the forward weak inequalities. If the reverse weak inequality held, transitivity would contradict one of the two strict hypotheses. The mixed strict–weak laws follow from the same argument.

Theorem 2.8 Equivalence from equivalent option lists

✓

Let \(a=\{ A^L\mid A^R\} \) and \(b=\{ B^L\mid B^R\} \) be games. Suppose

\[ \begin{aligned} & \forall a^L\in A^L,\ \exists b^L\in B^L,\quad a^L\sim b^L,\\ & \forall b^L\in B^L,\ \exists a^L\in A^L,\quad b^L\sim a^L,\\ & \forall a^R\in A^R,\ \exists b^R\in B^R,\quad a^R\sim b^R,\\ & \forall b^R\in B^R,\ \exists a^R\in A^R,\quad b^R\sim a^R. \end{aligned} \]

Then \(a\sim b\).

Proof ▶

We first verify the two clauses of Definition 2.4 for \(a\preceq b\). Let \(a^L\) be a left option of \(a\), and suppose that \(b\preceq a^L\). Choose a left option \(b^L\) of \(b\) such that \(a^L\sim b^L\). The forward inequality in this equivalence and transitivity from Theorem 2.7 give \(b\preceq b^L\). This is impossible: reflexivity from the same theorem gives \(b\preceq b\), whose left-option clause forbids \(b\preceq b^L\).

Next let \(b^R\) be a right option of \(b\), and suppose \(b^R\preceq a\). Choose a right option \(a^R\) of \(a\) such that \(b^R\sim a^R\). The reverse inequality \(a^R\preceq b^R\) in this equivalence and transitivity give \(a^R\preceq a\), contrary to the right-option clause of the reflexive comparison \(a\preceq a\). Thus \(a\preceq b\). Interchanging \(a\) and \(b\) proves \(b\preceq a\), and Definition 2.5 then gives \(a\sim b\).