John Horton Conway's book On Numbers and
Games introduces a formulation of the notion of number
which falls
naturally out of the approach he took to game theory. This arises more
naturally than the classical real
numbers and extends them gracefully to
embrace diverse infinities and infinitesimals. Wikipedia has an entry for the surreal numbers which
provides a nice clear description of what you get out of Conway's definitions.
It is possible to describe the surreals as mappings from ordinals to a two-member set, to be thought of as {+,−}. To interpret a mapping ({+,−}: f |n) with n ordinal as a surreal, first identify the maximal ordinal m subsumed by n for which ({+}:f|m) or ({−}:f|m), i.e. the first m entries in f are identical. We then interpret (:f:m) as m if ({+}:f|m) or as −m if ({−}:f|m); if m is 0 these both interpret (:f:m) as 0. If n > m, we know f(m) is the member of {+,−} that isn't in (|f:m); and interpret f as (:f:m) + sum(:f(i+m)/power(i,2) ←i:), subject to a suitable extension of power to transfinite ordinals. But I prefer to start from Conway's formulation, albeit transposed from his notation (which is optimized for discussion of games) to mine (which, for all its deficiencies, is at least consistent across everything I write).
Conway discovered the surreals in the course of studying the theory of deterministic two-player games: the surreals are a particular class of game. Actually, it'd more closely match normal understanding to refer to game positions: in any position of a game, for each of the players, we can consider the moves open to that player and, consequently, the set of positions that may result from that player's move. The game position may then be characterized by the two sets of positions that may result from the respective players' moves. If either player's set is empty, and it is that player's turn to move, then that player has lost the game. Otherwise, one can evaluate the positions open to the player whose turn it is; this player ideally chooses the best of these positions to play and it becomes the other player's turn.
Given only the characterization of positions in terms of the sets of
positions to which they can lead, it's possible to determine everything about
the strategy of a game. Now, of course, one can really start a game in any of
the positions to which it can lead, not just its orthodox starting position; so
the distinction between a position and a game becomes unimportant. So,
formally, Conway defines a game to be a pair of sets of games; one member of the
pair is termed its left set and the other its right set. If the game's name is
x then the denotation xR stands for any member of the right set of
x
; likewise xL is an arbitrary member of its left set.
Conway then goes on to define a partial ordering on games: x≤y iff there is no yR that's ≤ x and no xL that's ≥ y, where ≥ is reverse(≤). The intersection of ≥ and ≤ is an equivalence for which, if you replace one game with another equivalent to it, the dynamics may be radically different but the outcome is the same (at least when both players play optimally). Conway then establishes surreals as a sub-type of games, where each surreal is equivalent to some surreal which is a pair of sets of surreals (as distinct from more general games); and the union of ≤ and ≥ is the all-relation on surreals.
I want to transpose that into my notation and ways of formulating
mathematics, not because of any deficiency of Conway's but simply so that
everything on this site uses one consistent approach. Conway's formulation
requires a game to be a pair
of sets; which I could implement as a list
({sets}:|2) but prefer to implement as an atom W←X; and it's natural in my
formalism to have W and X be collections rather than sets, or indeed to consider
what relations I could use in their places. Since I'm only interested in the
surreals themselves, each of which is expressible as a pair of sets of surreals,
I'll skip the games entirely. So a surreal is a pair W←X in which W and X
are collections of surreals.
The mutually reverse relations ≤ and ≥, each ({surreals}::{surreals}), are essential to the discussion; for W←X to be a number, we require that no member of X is ≤ any member of W. Each surreal is then a pair W←X of collections of surreals for which (W:≥:X) is empty. (Note that, when X and W are non-empty, (W:≤:X) determines X and W entirely; but we can't use this as the representation of W←X because it's empty when either X or W is empty, losing all information about the other.) Given two such values, W←X and Y←Z, we have Y←Z ≥ W←X precisely if both ({W←X}:≥:Z) and (W:≥:{Y←Z}) are empty. Notice that left values only appear as left constraints and right values as right constraints, when constraining ≥. Once we've established that ≤ and ≥ are transitive and reflexive, we can intersect them to get an equivalence relation.
For a surreal W←X, we don't really need W and X to be collections: we can replace W with any relation which has the same right values as it and X with any relation which has the same left values as it. Any right value of W can be ignored if it's ≤ some other right value of W; likewise for any left value of X that's ≥ some other – and, conversely, we can add arbitrary surreals that shall be ignored to either side. Then again, as long as ≥ and ≤ are reflexive, each subsumes every collection of its values. So, in fact, instead of collections of surreals, we could use sub-relations of ≤ or of ≥ for X and Y. Still, since only the right values of W and left values of X are relevant, it's merely inconvenient to get a notionally distinct surreal when replacing W with some other relation having the same right values, or likewise X for left; so I'll restrict to collections.
So we define surreals and our relation ≥ on them inductively by:
We can define ≤ = reverse(≥). The members of the left value of a surreal number are known as its left options; the members of the right value of a surreal number are known as its right options; collectively, these are known as options of the surreal.
Once I've established that the intersection of ≤ and ≥ is an
equivalence relation, I'll use that as the proper notion of equality for
surreals, which =
shall then denote. When it is necessary to distinguish
is the same pair of collections of surreals
(implicitly meaning they have
the same
members in this same sense) from equality (as mediated by our
equivalence), I shall follow Conway in writing ≡ for the same pair
comparison.
A proposition about the surreals takes the form of a statement with names, quantified over by the proposition, standing for surreals: as such, it is an encoding of a family of statements obtained from it by consistently replacing each name with one surreal (and removing the wording that says to quantify over that name). Refer to each such statement as an instance of the proposition; and describe an instance as established if has been proven true. Likewise: any specification of a way to obtain a value from one or several surreals, whose values are arbitrary, uses names for these last and is, again, an encoding of a family of instances, each of which replaces each name consistently with one surreal. Describe an instance of a specification as established if the value of all expressions it implicates are fully and properly specified.
For the purposes of this section, I define a simplifying step
as a
transformation of such an instance in which the surreals it acts on (i.e uses in
place of the names in the proposition or specification) are optionally permuted
and one of them is replaced by one of its options. I'll describe one instance
of a proposition or specification as simpler than another if the former may be
arrived at from the latter by some sequence of simplifying steps.
The inductive principle used in specifying functions on the surreals and proving theorems about them is that, in establishing each instance, one may inductively presume that all simpler instances are established. The rationale for this is that there is no way to construct a surreal except in terms of simpler ones.
To map this principle formally onto the classical inductive approach,
classify surreals into ordinal-indexed generations
as follows: for any
ordinal n, generation n of the surreals comprises all surreals whose left and
right values are subsumed by the union, over ordinals m earlier than n, of
generation m. (Notice that each ordinal's generation is subsumed by that of any
later ordinal.) We can then associate each surreal with the intersection of all
ordinals for which the surreal is in that ordinal's generation (i.e. the first
such ordinal); describe this as the generation of the surreal. The tacit
presumption contained in the inductive principle is that every surreal is in
some ordinal's generation.
Consider a simple proposition or definition, H, conforming to our inductive principle and only implicating one surreal in each instance. We can prove H orthodoxly by induction on the generation of this surreal, since every simpler surreal has earlier generation. For more complex propositions and definitions, orthodoxy requires more complex multiple induction: but the added complexity is merely an artifact of the limitations of orthodox induction. The interested reader is welcome to convert the proofs and specifications below into the form required for this approach, but Conway's given inductive principle makes the proofs and specifications vastly more intelligible without any actual loss of rigour.
By way of illustrating how to use this inductive principle, let us now establish that ≥ does actually have two of the properties normally associated with operators using its name: it's reflexive (i.e. every surreal is ≥ itself) and transitive (i.e. u≥v and v≥w implies u≥w).
Proof: given a surreal W←X, we inductively suppose that every option of W←X is a fixed point of ≥. We need to show W←X ≤ W←X, i.e. ({W←X}:≥:X) = {} = (W:≥:{W←X}); and we know (W:≥:X) = {}. For the left half of this, there must be no x in X with W←X ≥ x, for which it suffices that each x in X has non-empty ({x}:≥:X), for example.
Every right option x of W←X is a member of X and a fixed point of ≥ hence a fixed point of ({x}:≥:X) which is consequently non-empty, so ({W←X}:≥:X) = {}. Every left option w of W←X is likewise a member of W and a fixed point of ≥ hence a fixed point of (W:≥:{w}), so (W:≥:{W←X}) = {}. We have thus proven that W←X ≥ W←X; thus any surreal whose options are fixed points of ≥ is itself a fixed point of ≥; hence every surreal is in fact a fixed point of ≥, i.e. ≥ is reflexive.
given u≥v and v≥w, we need to show u≥w. Let u
≡ U←X, v ≡ V←Y and w ≡ W←Z; we are given that,
among other restrictions of ≥, ({v}:≥:X) and (W:≥:{v}) are empty. For
any option s of w, our inductive principle allows us to presume that s≥u
(and u≥v) implies s≥v
, whence {s in W: s≥v} subsumes {s in W:
s≥u}. However, (W:≥:{v}) is given to be empty, hence so is {s in W:
s≥v}, hence so is its sub-collection {s in W: s≥u}, hence so is
(W:≥:{u}). Likewise, from our inductive principle, for any option s of u,
(v≥w and) w≥s implies v≥s
, whence {} = {s in X: v≥s} subsumes
{s in X: w≥s}, whence ({w}:≥:X) is also empty. But (W:≥:{u}) = {} =
({w}:≥:X) iff u≥w – QED.
The constructibility requirement, implied by the rationale for our inductive principle, obliges us to consider how we may construct some actual surreals, for which we'll need some collections of surreals. We inescapably have {} as a collection of surreals and it fatuously satisfies ({}:≥:{}) = {}, giving us {}←{} as a surreal. This lets us construct another collection of surreals, which we can use in constructing further surreals with which to construct further collections of surreals and so on.
From the definitions, for any collection X of surreals, (X:≥:{}) = {} = ({}:≥:X) fatuously, so X←{} and {}←X are surreals. Likewise, ({{}←{}}:≥:{}), ({}:≥:{X←{}}), ({}:≥:{{}←{}}) and ({{}←X}:≥:{}) are all empty so X←{} ≥ {}←{} ≥ {}←X.
Thus ≥ is reflexive and transitive, as are its reverse ≤ and their
intersection, which is necessarily an equivalence relation. Since every surreal
is a fixed point of ≥, hence also of ≤, every surreal is a fixed point of
this equivalence, i.e. equivalent to itself. Two surreals are deemed equal
precisely if this equivalence relates them to one another: x = y iff x≤y and
y≤x, for surreal x and y. Define relations < correspondingly by x<y
iff y≥x and ({x}:≥:{y}) is empty
(those more relaxed than me about
reductio can read not(x≥y) where I say
({x}:≥:{y}) is empty
) and let > be its reverse.
Now, transitivity of ≥ implies that, for given collections X, Y, Z of surreals, (X:≥:Z) subsumes (X:≥:Y)&on;(Y:≥:Z), since the latter relates a right value x of X to a left value z of Z precisely if ≥ relates x to some y in Y which ≥ relates to z, i.e. x≥y≥z, which implies x≥z. Further, if (X:≥:Z) is empty and either (X:≥|Y) or (Y|≥:Z) then (respectively) (Y:≥:Z) or (X:≥:Y) must be empty. For the first case: {} = (X:≥:Z) subsumes (X:≥|Y)&on;(Y:≥:Z); for any y in Y, there's an x in X with x≥y and any surreal v with y≥v also has x≥v, whence v is not in Z; so (Y:≥:Z) is empty. The second case, {} = (X:≥:Z) with (Y|≥:Z) implies (X:≥:Y) = {}, is similar. I shall use this result extensively below.
Theorem: surreal x ≡ W←Y implies (W|<:{x}) and ({x}:<|Y).
we have x≥x, so ({x}:≥:Y) = {} = (W:≥:{x}). For any w in W or y in Y we thus have ({x}:≥:{y}) = {} = ({w}:≥:{x}) as required for y>x>w; it remains to show y≥x≥w. Since x is surreal, (W:≥:Y) = {} so ({w}:≥:Y) = {} = (W:≥:{y}). Suppose w ≡ U←V; our inductive principle lets us assert that (U|<:{w}), whence ({w}:≥|U); and {} = (W:≥:{x}) subsumes ({w}:≥{x}) subsumes ({w}:≥|U)&on;(U:≥:{x}), whence (U:≥:{x}) is empty; taken with ({w}:≥:Y) = {}, this implies x≥w. Likewise with y = U←V we get ({y}:<|V) so (V|≥:{y}); and {} = ({x}:≥:Y) subsumes ({x}:≥:{y}) subsumes ({x}:≥:V)&on;(V|&on;:{y}), so ({x}:≥:V) is empty, as was (W:≥:{y}), so y≥x – QED.
Theorem: given surreals x, y, either x≥y or y≥x.
let x ≡ W←X and y ≡ Y←Z. From the definition, x≥y iff ({y}:≥:X) = {} = (Y:≥:{x}) so we have three possibilities: x≥y or; there is some v in Y with v≥x or; there is some u in X with y≥u. Now v in Y implies v<y and u in X implies x<u so our three cases reduce to: x≥y or y>v≥x or y≥u>x and the last two both imply y≥x – QED.
Thus our comparisons constitute a total order on surreals. Note that the
proof actually gives us x≥y or y>x directly; but, in any case, the theorem
itself implies this since x≥y or y≥x
implies x≥y or
which is exactly the statement y≥x
and not(x≥y)
x≥y or y>x
from the definition of >.
It remains, for this section, to prove that when two surreals are
equivalent, replacing one with the other as an option of a third surreal yields
a surreal equal to this third – that is, our equivalence
is good
for what we want of it. I shall deal with this by proving a stronger result.
Theorem: given surreal W←Y and collections V and Z of
surreals; (W|≤:V), (V|≤:W), (Y|≥:Z) and (Z|≥:Y)
implies
V←Z is surreal and W←Y = V←Z.
W←Y is surreal implies {} = (W:≥:Y), which subsumes (W:≥:Z)&on;(Z|≥:Y) whence {} = (W:≥:Z) which subsumes (W:≥|V)&on;(V:≥Z) so (V:≥:Z) is empty and V←Z is surreal.
We can define negation remarkably easily: given a surreal x ≡ W←Y,
Written by Eddy.