Conway's ideas have been taken up and pursued by a few others (eg. Knuth, Gonshor, Kruskal, Joyal, game theorists, Ehrlich). To me they raise some fascinating questions in computer science, proof theory, and other fields. How about nonterminating games? What are the implications of confining winning strategies to be written in a particular formal system? And so on.
Here I will simply write down a definition of the kind of games considered by Conway, and his arithmetic operations +, * and -. If you want to read something much better written, see this wikipedia article. or this article (pdf).
The games are defined inductively, in a manner reminiscent of Peter Aczel's `tree set' interpretation of constructive ZF in Martin-Löfs type theory. In preparation, here is a brief sketch of this interpretation.
{ T(u) | u : U } closed
under a suitable set of set-forming operators (0, 1, +, Sigma, Pi,
what have you - I won't be specific), and interprets `epsilon' sets
using well founded trees of type W(U,T), where W
is Martin-Löf's well-ordering `quantifier', ie the least
solution X of
X = (Sigma u : U) T(u) -> X
with typical element
sup(u,f)
where u : U, f : T(u) -> W(U,T)
To (over-)simplify, he defines the epsilon relation .eps. , and the
auxiliary relations of inclusion .sub. and equality
.eq. between trees in W(U,T) recursively. (Well,
actually, he's more careful than that. See below.) The idea
is
x .eps. sup(u,f) == (Sigma t : T(u)) x .eq. f(t)
sup(u,f) .sub. y == (Pi z : T(u)) f(t) .eps. y
x .eq. y == x .sub. y /\ y .sub. x
Then one proves that .eq. is an equivalence relation
compatible with .eps. and .sub.; then we
figure out which set-theoretical axioms hold, depending on
the closure properties of the universe (U,T).
(To really formalise the construction in some version of Martin-Löf
type theory, one has to be more careful -- as Aczel was. See for
example "The type-theoretic interpretation of constructive set theory:
Choice Sequences", in "The L.E.J.Brouwer Centenary Symposium",
North-Holland 1982, eds. Troelstra, van Dalen. From memory, one has
to define for each a : W(U,T) the pair of predicates
((a .sub.), (.sub. a)) by recursion. By defining both
predicates together, one has access to .eq..)
W2
of the W quantifier, where W2(U,T) is the
least solution X of
X = ((Sigma uL : U) T(uL) -> X) * ((Sigma uR : U) T(u) -> X)
(The symbol * means binary Cartesian product) with
typical element
sup2(uL, fL, uR, fR)
where uL, uR : U,
fL : T(uL) -> W2(U,T), fR : T(uR) -> W2(U,T)
Such things might perhaps be called bi-trees. As it were, we have
`sets' with 2 kinds (or `colours') of epsilon relation. How are these
games? Actually they are positions in games. The games are
played between 2 players, which we call `L' and `R'. If it is L's go,
then she can move to any of the positions { fL(t) | t : T(uL)
} and (natch) if is R's go, she can move to any of {
fR(t) | t : T(uR) }. Then they take turns. The first player
who cannot move (their family being empty) `loses', and the other
`wins'. Since W2 is inductively defined, one or other of
the players will inevitably win.
An interesting thing about the Conway games is that either player can go first; in other structures I have thought about eg here) it is `built in' that one or other of the players goes first.
L (resp. R) has a
winning strategy. (It is also possible that the first player can win -
such games are called `fuzzy'. Conway does not count them as numbers,
though they are interesting as games.)
To define the arithmetic operations +,*,-, it
helps to use Conway's own `cut' notation. He writes a game position
in the form
x = { .., xL, .. | .., xR, .. }
where xL denotes (the destination position of) a typical one of L's moves,
and xR similarly one of R's.
Then (recursively):
x + y == { .., xL + y, .. , x + yL, ..
| .., x + yR, .. , xR + y, .. }
x * y == { .., xL*y + x*yL - xL*yL, .. , xR*y + x*yR - xR*yR, ..
| .., xL*y + x*yR - xL*yR, .. , xR*y + x*yL - xR*yL, .. }
- x == { .., - xR, .. | .. , - xL, .. }
(When the definitions are written out with full logical hygiene, it
must be assumed that the universe of sets (U,T) is closed
under binary disjoint union.) (There seems to be a typo in the
definition of product on p. 291 of Conway and Guy's "The book of
numbers".) The intuition for + is clearly a kind of
interleaving between the two summands. I don't understand
* well enough to say anything about it. Minus is a
systematic swapping of roles between the two players. (Conway
considers a lot of other operators on games, including one which is
much closer to the ordinary non-commutative ordinal sum
than +.)
Here is one approach to dealing with Conway games in Haskell.
One can then define an equivalence relation (like strong bisimulation)
between game positions x and y , which
equates them if x - y has zero value (ie. the second
player to move has a winning strategy). When quotiented by this
relation, and supplemented by analogously defined order relations, it
turns out, astoundingly, that (non-fuzzy) game positions form a
linearly ordered real-closed field, with a very strong universal
embedding property. (A field is formally real if -1 is
not a sum of squares, and real closed if it in addition it has no
proper formally real algebraic extensions.) There are the so-called
"surreal" numbers (so-called by Knuth), that includes not only
transfinite ordinals, but their reciprocals, roots, powers,
logarithms, factorials, and so on. (Exactly what
we get depends on the universe we start with.)
Joyal has considered yet another definition of +:
x + y == { .., xL + y, .. | .., x + yR, .. }
Note the difference from Conway's definition: he ignores leftmoves in y
and rightmoves in x. Can this be right??
He defines (recursively) two sets of strategies: S0(x)
(the set of winning strategies for the left player when they go
second) and S1(x) (the set of winning strategies for the
left player when they go first):
S0(x) == (Pi xR) S1(xR)
S1(x) == (Sigma xL) S0(xL)
Joyal shows that if one defines a morphism from x to y
to be an element of S0(y + (-x)), then one has a monoidal, closed,
symmetric(??) and auto-dual category.
Also interesting is the `two epsilons' set theory to which Conway tantalisingly alludes on p. 66 of his book. (It may be useful to think of the indices of the two families in a bi-tree as `actions' and `co-actions', in the spirit of Milner's CCS.) What would an axiomatision of 2-epsilon set theory look like?
A philosopher with an interesting perspective on surreal arithmetic, generalised continua, "the infinite" and so on is Philip Ehrlich. He alludes to "a vast generalisation of Cantor's theory of arithmetic". It sounds as if he has something more general than Conway's surreals; unfortunately, he doesn't put his papers online.
Andre Joyal has apparently given a category-theoretic description of
Conway games. (There is a short paper from 1977.) According to a
paper by Martin Hyland(??) they form a `compact closed' category. I
think the definition of the hom-sets is based on the properties of
addition. I don't know what a compact closed category is but I've the
impression it is a rather grotty mechanistic kind of category.
Perhaps one gets a category with better properties by allowing that
games needn't terminate? Then the aritmetic operations can no longer
be defined by well-founded induction. Instead of an initial algebra
for S |-> (Fam S)^2 one might look instead at final
coalgebras for this or some other functor. This raises questions of
what happens to the concepts of winning and losing. My feeling is
that one should focus on the notion of having a strategy to avoid
losing, which is being driven or painted into "a corner" in which
there is no further room for maneuver, or deadlock.
Read the book!