# How to define Conway's class of all games rigorously?

I'm reading John Conway's On Numbers And Games.

In the course of defining the surreal numbers, Conway defines the term game more or less as follows.

• $(\emptyset,\emptyset)$ is a game.
• If $L$ and $R$ are sets whose elements are games, then $(L,R)$ is a game.
• All games are constructed in this way.

Obviously this is an informal definition, so I'd like to see a formalized version. However, the 'solution' to this problem discussed in the Appendix to Part 0 doesn't make sense to me.

Can someone provide a formal definition of the predicate $\mathrm{Game}$ which returns true iff the input is a game?

Note that the issue here is quite distinct from the issue discussed here: are surreal numbers actually well-defined in ZFC?.

What I've tried so far. It's tempting to proceed as follows. Define that a class $C$ is closed iff whenever $L$ and $R$ are sets with $L,R \subseteq C,$ then $(L,R) \in C.$ Then the class of games is defined as the intersection of all closed classes incorporating $(\emptyset,\emptyset)$.

There's a few issues with this. Firstly, in ZFC, we don't have classes, just predicates. So, how do we rehash the notion of an intersection of all closed classes in terms of predicates? Is it even possible? I'm willing to use NBG or MK if its strictly necessary, but I don't think it is.

Secondly, how do we know there exists a closed class? We don't want to use the cumulative hierarchy to construct such a class, because the whole point of Conway's approach is that we get the ordinals for free as a subset of the surreals.

Edit. In the comments, it was mentioned that $\in$-recursion makes Conway's definition rigorous. Can someone explain precisely how this is done?

For instance, does $\in$-recursion allow us to define 'game' by asserting that $x$ is a game iff there exist sets $L,R$ such that $(L,R)=x$ and the elements of $L$ and $R$ are games.

• Transfinite recursion (more precisely, $\in$-recursion) makes this «obviously informal definition» absolutely formal. Jun 22 '13 at 13:51
• I'm reading up the very same thing!! This is a very helpful pdf. It presents a formal mathematical approach to the whole issue in a succint manner. Not sure this is exactly what you're looking for though.
– user67803
Jun 22 '13 at 13:54
• To slightly expand on @Grigory's comment, much like we can define $\omega$ as the intersection of all inductive classes (even without the axiom of infinity), we can also define it as the set generated by $\varnothing$ and $x\mapsto x\cup\{x\}$. This gives us a method to define the class of games from $(\varnothing,\varnothing)$ using transfinite recursion. And a second-order argument would show that the result is the same as taking the intersection of all closed classes. Jun 22 '13 at 13:57
• @GrigoryM: Can you carry out this transfinite recursion without the ordinals already in place? (I'm not saying you can't, only that it is not obvious to me how you would do so.) Jun 22 '13 at 14:08
• @Charles: You don't do this induction over the ordinals, you do it over the well-foundedness of $\in$ (given by the axiom of regularity) and the relevant axioms of replacement. Jun 22 '13 at 15:07

I'll begin with an auxiliary definition, that I'll call "evidence"; the intuition is that a set is evidence if it contains enough information to verify that each of its elements is a game. Formally, a set $E$ is evidence if it is a set of ordered pairs and, for each pair $(L,R)\in E$, both $L$ and $R$ are sets and all their members are also in $E$. [Technically, I could omit the clause "both $L$ and $R$ are sets," because in ZF everything is a set, but I think the definition is easier to understand with that clause included.] Note that this is an explicit definition of what it means for a set to be evidence.
Now define a set $G$ to be a game iff it is a member of some $E$ that is evidence.
• Andreas I am trying to show that evidence sets are well-ordered. Can I have a little help? I need to show that, given arbitrary non-empty collection of evidence sets $\mathcal{E}$ and setting $F = \bigcap \mathcal{E},$ we have $F \in \mathcal{E}$. Just a little hint or a pointer should be enough. Jun 24 '13 at 13:50
• @user18921 Yes, induction works fine; this is just an explicit definition of the same notion of game, not an introduction of a new notion. To formalize an inductive proof of "all games have property X" in this framework, you could show that, whenever $E$ is evidence, all its members $G$ have property X. That proof could go by induction on the set-theoretic rank of $G$. Jul 16 '13 at 14:43