ON CONWAY NUMBERS AND GENERALIZED REAL NUMBERS Conway’s Theory of Games and Numbers Constructively Reconstructed

Frank Rosemeier

FernUniversität Hagen Postfach 9 40 D-58084 Hagen (Germany)

frank.rosemeier@fernuni-hagen.de

Keywords: Constructive mathematics, Conway games, Conway numbers. MSC2000: 03F65 (03H15, 91A05) Abstract John Horton Conway presents in his book “On Numbers and Games” a

general method to create a class of numbers containing all real numbers as well as every ordinal number. Using the logical law of excluded middle (LEM) he equips this class with the structure of a totally ordered field. This paper is a first step to investigate the contribution of Conway’s theory to the foundations of Constructive Nonstandard Analysis. In his book Conway suggests defining real numbers as (Conway) cuts in the set of rational numbers. Following his ideas, a constructive notion of real numbers will be developed. Parallels to and differences from the concept of generalized real numbers recently published by Fred Richman [Indag. Mathem., N. S., 9 (4) 595-606 (1998)] will be outlined.

Introduction

In his book “On Numbers and Games” [2] John H. Conway develops a very general theory of numbers and games, frequently using the logical law of excluded middle (LEM). This paper aims to start a constructive investigation of this theory. Following his ideas, constructive notions for Conway games and Conway numbers will be developed and a constructive version of Conway’s theory will be given. We shall mark any application of (LEM), constructively rejected omniscience or choice principles are avoided. Whether the author’s aim to avoid even countable choice has been achieved may be judged by mathematicians with more experience in working without choice. (Fred Richman suggested to drop countable choice at the Antipodes-Symposion, cf. also [7] and [9].)

Conway games are defined in Section 1 and operations of addition and subtraction for such games are presented in Section 2 resp. 3. The relations of order and equality are shown to have the expected properties in Sections 4–5. Section 6 (resp. 7) deals with (real) Conway numbers. In Section 8 real Conway numbers are compared with generalized Dedekind reals (cf. [6] and [9]).

1. CONWAY GAMES

1.1 Motivation. Conway games are played by two players (usually called Left and Right) moving alternately according to specific rules without chance moves and without hidden information. Such a game is characterized by the positions each of the two players can reach from any position with the next move. Thus, a Conway game x will be described by two sets L_{x} and R_{x}, the sets of Left resp. Right options (i. e. positions reachable by Left resp. Right from the starting position of x within one move). As every position P in a game x can be identified with the shortened game x_{P} (which is played according to the rules of x starting from position P) the sets L_{x} and R_{x} will be identified with sets of Conway games. Vice versa, whenever L and R are sets of Conway games, we can construct a new Conway game {L|R}, in which Left may move to any element of L whereas Right may move to any element of R. Having this in mind the following definition can be given.

1.2 Definition. (Conway games) For every set X let Γ(X) := P(X) × P(X) be the set of pairs of subsets

of X. Define  G_{0} := Γ(∅), G_{1} := Γ(G_{0}), G_{2} := Γ(G_{1}), … G_{ω}:= Γ( ⋃_{k=0}^{∞} G_{k}), G_{ω+1} := Γ(G_{ω}), etc.

i. e. define G_{α+1} := Γ(G_{α}) for every ordinal α, and for any lim-ordinal λ define G_{λ} := Γ (⋃ { G_{α} : α contained in λ }). (Containment is introduced in A.3 of [8], where the appendix presents a constructive notion of ordinal numbers which is compatible with constructive Conway theory.)

Ug_{j} := ⋃ { G_{α} : α ∈ On_{j} } may be called j-th (Conway) game class (j ∈ ℕ_{0}), and elements of Ug_{⋆} := ⋃_{j=0}^{∞} Ug_{j} are (Conway) games. (Conway denotes by Ug his proper class of “unimpartial” games, i. e. games possibly favouring one of the players, cf. [2] p. 78. The ordinal number classes On_{j} corresponding to the ordinals ω_{j−1} are defined in A.2 of [8].)

1.3 Notation. (Left/Right Options) The projections pr_{L} : Ug_{⋆} → Ug_{⋆}, (L, R) ↦ L and pr_{R} : Ug_{⋆} → Ug_{⋆}, (L, R) ↦ R are used to define two sets of games for every game x ∈ Ug_{⋆}:

L_{x} := pr_{L}(x) and R_{x} := pr_{R}(x), the set of Left resp. Right options in x. Two games are called identical if their sets of Left options and their sets of Right options coincide: x ≡ y :⟺ L_{x} = L_{y} and R_{x} = R_{y} (x and y have the same form). If x ≡ (L_{x}, R_{x}) is a game, x^{L} will be a typical element of L_{x} (typical Left option) and x^{R} will be a typical element of R_{x} (typical Right option).

Let {x_{1}, …, x_{n}|y_{1}, …, y_{m}} abbreviate ({x_{1}, …, x_{n}} , {y_{1}, …, y_{m}}). Instead of y ≡ ({z} , ∅) we will write y ≡ {z|} etc. Sometimes the expression {x^{L}|x^{R}} will be used as notation for the game x.

1.4 Examples. (The four simplest games)

(1) ⊥ ≡ {|} ≡ (∅, ∅), the empty game, in which both players are unable to move, is the only element of Ug_{0}.

(2) 1_{L} ≡ {⊥|} ≡ ({⊥} , ∅), the Left unit game, in which Left has a move to ⊥ while Right is unable to move, is an element of Ug_{1};

(3) 1_{R} ≡ {|⊥} ≡ (∅, {⊥}), the Right unit game, in which Right has a move to ⊥ while Left is unable to move, is an element of Ug_{1};

(4) ∗ ≡ {⊥|⊥} ≡ ({⊥} , {⊥}), the Nim unit game, in which both players have a move to ⊥, is an element of Ug_{1}. (Nim is described in [1].)

1.5 Convention. (Normal play convention) A player unable to move loses, the other player is the winner. (No game can go on forever, cf. the Descending Chain Condition in A.3 of [8].)

1.6 Definition. (Outcome classes) For any x ∈ Ug_{⋆} define (a game theoretic interpretation is given in 1.7)

x ≥ 0 :⟺ ∀ x^{R} ∈ R_{x} : x^{R} ▷ 0 (Left can win if Right starts),
x ▷ 0 :⟺ ∃ x^{L} ∈ L_{x} : x^{L} ≥ 0 (Left can win if Left starts),
x ≤ 0 :⟺ ∀ x^{L} ∈ L_{x} : x^{L} ◁ 0 (Right can win if Left starts),
x ◁ 0 :⟺ ∃ x^{R} ∈ R_{x} : x^{R} ≤ 0 (Right can win if Right starts),
x > 0 :⟺ x ≥ 0 and x ▷ 0 (x is positive, Left can win),
x < 0 :⟺ x ≤ 0 and x ◁ 0 (x is negative, Right can win),
x ∥ 0 :⟺ x ▷ 0 and x ◁ 0  (x is fuzzy, the first player can win),
x = 0 :⟺ x ≥ 0 and x ≤ 0 (x is zero, the second player can win).

(Here ‘can win’ stands for ‘has a winning strategy’. Readers who rely on this intuitive concept may prefer to define the outcome classes by the expresssions in parentheses; they can arrive at the formal definition given here by considering 1.7. Other readers may use the formal definitions given here to make precise the concept of winning strategy using 1.7.)

1.7 Remark. Left can win x in case Right moves first (i. e. x ≥ 0) if all possible Right moves lead to games which Left can win, provided Left is allowed to make the first move there. Left can win x in case Left moves first (i. e. x ▷ 0) if there is a Left (winning) move leading to a game which Left can win, provided Right has to move first there. Interpret the outcome classes in favour of Right (x ≤ 0, x ◁ 0) analoguously.

1.8 Examples. The outcome classes for the games from 1.4:

(1) ⊥ = 0 as both players are unable to move in ⊥;
(2) 1_{L} > 0 as Left wins (by moving to ⊥ or since Right has no move);
(3) 1_{R} < 0 as Right wins (by moving to ⊥ or since Left has no move);
(4) ∗ ∥ 0 as the first player wins by moving to ⊥.

1.9 Proposition.

(1) For all games x ∈ Ug_{⋆} we have

(i) ¬(x ≥ 0 and x ◁ 0), (ii) ¬(x ≤ 0 and x ▷ 0).

(2) The logical law of excluded middle,

(LEM) ψ or ¬ψ for every proposition ψ, is equivalent to each of the following statements:

(a) x ≥ 0 or x ◁ 0 for all x ∈ Ug_{⋆},

(b) x ≤ 0 or x ▷ 0 for all x ∈ Ug_{⋆}.

Proof: (1): (i) and (ii) are proved by mutual game induction, i. e. by game induction (transfinite induction on α ∈ On_{j}, j ∈ ℕ_{0}, x ∈ G_{α}) for the conjunction of (i) and (ii); the induction basis will not be mentioned as there are no options of {|}, the only element of G_{0} = Γ(∅). Ind. Step: (i) Suppose we have x ≥ 0 and x ◁ 0, hence x^{R} ▷ 0 for all x^{R} ∈ R_{x} and x^{R} ≤ 0 for some x^{R} ∈ R_{x}; but x^{R} ▷ 0 and x^{R} ≤ 0 would contradict Ind. Hyp. (ii). (ii) x ≤ 0 and x ▷ 0 would yield similarly a contradiction to Ind. Hyp. (i). (2): “(LEM) ⟹ (a), (b)” is also proved by mutual game induction: Since ¬(x ◁ 0) ⟹ ¬(∃ x^{R} ∈ R_{x} : x^{R} ≤ 0) ⟹ ∀ x^{R} ∈ R_{x} : ¬(x^{R} ≤ 0) ⟹ ∀ x^{R} ∈ R_{x} : x^{R} ▷ 0 [by Ind. Hyp. (b)] ⟹ x ≥ 0,

we can deduce (a) from (LEM) via ( x ◁ 0 or ¬(x ◁ 0) ); (b) is deduced similarly from (LEM) and Ind. Hyp. (a). “(a) ⟹ (LEM)”: Let x_{ψ} ≡ (∅, R_{ψ}) ∈ Ug_{⋆}, R_{ψ} := { x ∈ {⊥} : ψ }, then

\begin{aligned}x_{ψ} ≥ 0 & ⟺ & ∀ y ∈ R_{ψ} : y ▷ 0 & ⟺ & ⊥ ∉ \{ x ∈ \{⊥\} : ψ \} & ⟺ & ¬ψ and \\ x_{ψ} ◁ 0 & ⟺ & ∃ y ∈ R_{ψ} : y ≤ 0 & ⟺ & ⊥ ∈ \{ x ∈ \{⊥\} : ψ \} & ⟺ & ψ. \end{aligned}

“(b) ⟹ (LEM)” is proved analogously. □

2. ADDITION

2.1 Motivation. Two games x, y ∈ Ug_{⋆} are played simultaneously by the simultaneous play rule: The player to move may choose from the allowed moves in exactly one of the components x or y leaving the other component unchanged. This leads to the following inductive definition.

2.2 Definition. (Addition of Conway games) For games x, y ∈ Ug_{⋆} their (disjunctive) sum is x+y ≡ (L_{x+y}, R_{x+y}) with L_{x+y} := (L_{x} +y)∪(x+L_{y}) = { x^{L} + y : x^{L} ∈ L_{x} }∪{ x + y^{L} : y^{L} ∈ L_{y} }, R_{x+y} := (R_{x}+y)∪(x+R_{y}) = { x^{R} + y : x^{R} ∈ R_{x} }∪{ x + y^{R} : y^{R} ∈ R_{y} }; we write concisely x + y ≡ {x^{L} + y, x + y^{L}|x^{R} + y, x + y^{R}}.

2.3 Remark. For all α, β ∈ On_{j}, j ∈ ℕ_{0}, we find γ ∈ On_{j} with x + y ∈ G_{γ} whenever x ∈ G_{α}, y ∈ G_{β}; hence add_{Ug_{⋆}} : Ug_{⋆} × Ug_{⋆} → Ug_{⋆}, (x, y) ↦ x + y satisfies add_{Ug_{⋆}}(x, y) ∈ Ug_{j} for all x, y ∈ Ug_{j}, j ∈ ℕ_{0}.

2.4 Examples.

(1) ⊥ + ⊥ ≡ {|} + {|} ≡ {|} ≡ ⊥;
(2) 1_{L} + ⊥ ≡ {⊥|} + {|} ≡ {⊥ + ⊥|} ≡ 1_{L} by (1);
(3) ⊥ + 1_{R} ≡ 1_{R} can be seen similarly;
(4) 1_{L} + 1_{R} ≡ {⊥ + 1_{R}|1_{L} + ⊥} ≡ {1_{R}|1_{L}} by (2) and (3).

2.5 Proposition. (Ug_{⋆} monoid) Ug_{⋆} is a commutative monoid with neutral element ⊥ ≡ {|}: For all games x, y, z ∈ Ug_{⋆} we have

\begin{aligned}(1) & x + ⊥ & ≡ x, \\ (2) & x + y & ≡ y + x, \\ (3) & (x + y) + z & ≡ x + (y + z). \end{aligned}

Proof: The proofs are carried out by ordinary game inductions: (1): x + ⊥ ≡ {x^{L} + ⊥|x^{R} + ⊥} ≡ {x^{L}|x^{R}} [Ind. Hyp.] ≡ x. (2): y + x ≡ {y^{L} + x, y + x^{L}|y^{R} + x, y + x^{R}} ≡ {x + y^{L}, x^{L} + y|x + y^{R}, x^{R} + y} [Ind. Hyp.] ≡ x + y.

(3): (x + y) + z ≡ {(x^{L} + y) + z, (x + y^{L}) + z, (x + y) + z^{L}|…} ≡ {x^{L} + (y + z), x + (y^{L} + z), x + (y + z^{L})|…} [Ind. Hyp.] ≡ x + (y + z). □

2.6 Lemma. (Outcome classes and addition) For all games x, y ∈ Ug_{⋆} the following statements hold.

\begin{matrix}(1) & x ≥ 0 and y ≥ 0 ⟹ x + y ≥ 0, \\ (2) & x ≥ 0 and y ▷ 0 ⟹ x + y ▷ 0, \end{matrix}

(3) x + y ≥ 0 and y ≤ 0 ⟹ x ≥ 0,
(4) x + y ≥ 0 and y ◁ 0 ⟹ x ▷ 0,
(5) x + y ▷ 0 and y ≤ 0 ⟹ x ▷ 0.

(2.7 gives a game theoretic interpretation of some of these implications.)

Proof:

(1) and (2) are mutually proved by a straightforward game induction. (3), (4) and (5) are also proved by mutual game induction (cf. 1.9):

(3): x + y ≥ 0 ⟹ ∀ x^{R} ∈ R_{x} : x^{R} + y ▷ 0
⟹ ∀ x^{R} ∈ R_{x} : x^{R} ▷ 0 [by Ind. Hyp. (5)].
(4): x + y ≥ 0 ⟹ ∀ y^{R} ∈ R_{y} : x + y^{R} ▷ 0
⟹ x ▷ 0 [by Ind. Hyp. (5)],

because y ◁ 0 ⟹ ∃ y^{R} ∈ R_{y} : y^{R} ≤ 0.

(5): x + y ▷ 0 ⟹ ∃ x^{L} ∈ L_{x} : x^{L} + y ≥ 0 or ∃ y^{L} ∈ L_{y} : x + y^{L} ≥ 0;
first case: ∃ x^{L} ∈ L_{x} : x^{L} + y ≥ 0 ⟹ x^{L} ≥ 0 [by Ind. Hyp. (3)];
second case: ∃ y^{L} ∈ L_{y} : x + y^{L} ≥ 0 ⟹ x ▷ 0 [by Ind. Hyp. (4)],

because y ≤ 0 ⟹ ∀ y^{L} ∈ L_{y} : y^{L} ◁ 0. □

2.7 Interpretation. The first implication of 2.6 asserts that Left can win the sum if Right starts, provided Left can win each component. Indeed, Left can find a good reply to any move of Right because there is a good reply in any component, thus Left will win by choosing always the same component as Right and playing a winning move there. The second implication of 2.6 means that Left having the first move can win the sum x+y, provided Left can win one component x with Right moving first and the other component y having the first move. Indeed, Left may start with a move from x + y to x + y^{L} ≥ 0 choosing a winning move y^{L} ≥ 0 in y. Interpret the remaining implications of 2.6 analogously.

3. SUBTRACTION

3.1 Motivation. The antigame −x is played like the original game x in which the roles of Left and Right have been interchanged: The allowed moves for Left in −x correspond to the Right moves in x and the allowed moves for Right in −x correspond to the Left moves in x, where the roles have to be interchanged in the options too. The following definition formalizes this idea.

3.2 Definition. (Subtraction) For every game x ∈ Ug_{⋆} its antigame is given by −x ≡ (L_{−x}, R_{−x}) with L_{−x} := −R_{x} = { −x^{R} : x^{R} ∈ R_{x} } and R_{−x} := −L_{x} = { −x^{L} : x^{L} ∈ L_{x} }; we write concisely −x ≡ {−x^{R}|−x^{L}}. The difference of x, y ∈ Ug_{⋆} is x − y ≡ x + (−y) ≡ {x^{L} − y, x − y^{R}|x^{R} − y, x − y^{L}}.

3.3 Remark. We have −x ∈ Ug_{j} whenever x ∈ Ug_{j}, j ∈ ℕ_{0}; using add_{Ug_{⋆}} from 2.3 we obtain sub_{Ug_{⋆}} : Ug_{⋆} × Ug_{⋆} → Ug_{⋆}, (x, y) ↦ x − y with sub_{Ug_{⋆}}(x, y) ≡ add_{Ug_{⋆}}(x, −y) ∈ Ug_{j} whenever x, y ∈ Ug_{j}, j ∈ ℕ_{0}.

3.4 Examples.

(1)  −⊥ ≡ −{|} ≡ {|} ≡ ⊥;
(2)  −1_{L} ≡ − {⊥|} ≡ {|−⊥} ≡ 1_{R} by (1);
(3)  −∗ ≡ − {⊥|⊥} ≡ {−⊥|−⊥} ≡ ∗ by (1);
(4) 1_{L} − 1_{L} ≡ 1_{L} + 1_{R} ≡ {1_{R}|1_{L}} by (2) and 2.4 (4).

3.5 Note. For all games x ∈ Ug_{⋆} we have

\begin{aligned}(1) & x & ≤ & 0 & ⟺ & −x & ≥ & 0, \\ (2) & x & ◁ & 0 & ⟺ & −x & ▷ & 0, \\ (3) & x & < & 0 & ⟺ & −x & > & 0. \end{aligned}

((1) and (2) are proved by mutual game induction, then (3) follows.)

3.6 Proposition. For all games x, y ∈ Ug_{⋆} the following statements hold.

\begin{aligned}(1) & −(−x) & ≡ x, \\ (2) & −(x + y) & ≡ (−x) + (−y), \\ (3) & −(x − y) & ≡ y − x, \\ (4) & x − x & = 0. \end{aligned}

(Example 3.4 (4) shows that (4) cannot be replaced by x − x ≡ ⊥.)

Proof: The proofs of (1) and (2) are carried out by ordinary game inductions:

(1) −(−x) ≡ − {−x^{R}|−x^{L}} ≡ {−(−x^{L})|−(−x^{R})} [Ind. Hyp.] ≡ x .

(2) −(x + y) ≡ {−(x^{R} + y), −(x + y^{R})|−(x^{L} + y), −(x + y^{L})} ≡ {(−x^{R}) + (−y), (−x) + (−y^{R})|(−x^{L}) + (−y), (−x) + (−y^{L})} [Ind. Hyp.] ≡ (−x) + (−y).

(3) is a consequence of (1), (2) and 2.5 (2). (4): We prove x − x ≤ 0. (This, (3) and 3.5 (1) yields x − x ≥ 0.)

We have x^{L} − x ◁ 0 for all x^{L} ∈ L_{x} as x^{L} − x^{L} ≤ 0 by Ind. Hyp. and we have x − x^{R} ◁ 0 for all x^{R} ∈ R_{x} as x^{R} − x^{R} ≤ 0 by Ind. Hyp. Hence (x − x)^{L} ◁ 0 holds for all (x − x)^{L} ∈ L_{x−x}, i. e. x − x ≤ 0. □

4. ORDER

4.1 Definition. (Order) For games x, y ∈ Ug_{⋆} define

x ≥ y :⟺ x − y ≥ 0 (x is at least as favourable for Left as y),
x ≤ y :⟺ x − y ≤ 0 (x is at most as favourable for Left as y),
x ▷ y :⟺ x − y ▷ 0 (x is partly more favourable for Left than y),
x ◁ y :⟺ x − y ◁ 0 (x is partly less favourable for Left than y),
x > y :⟺ x − y > 0 (x is more favourable for Left than y),
x < y :⟺ x − y < 0 (x is less favourable for Left than y),
x = y :⟺ x − y = 0 (x and y are equally favourable for Left),
x ∥ y :⟺ x − y ∥ 0 (x and y are incompatible).

4.2 Hint. For all games x, y ∈ Ug_{⋆} we have

\begin{aligned}(1) & x ≤ y & ⟺ y ≥ x ⟺ −x ≥ −y, \\ (2) & x ◁ y & ⟺ y ▷ x ⟺ −x ▷ −y, \\ (3) & x < y & ⟺ y > x ⟺ −x > −y. \end{aligned}

(The proofs are straightforward with 3.5 and 3.6.) 4.3 Lemma. (Characterization of order) For all games x, y ∈ Ug_{⋆} the following statements hold.

(1) x ≤ y ⟺ ∀ x^{L} ∈ L_{x} : x^{L} ◁ y and ∀ y^{R} ∈ R_{y} : x ◁ y^{R},
(2) x ◁ y ⟺ ∃ x^{R} ∈ R_{x} : x^{R} ≤ y or ∃ y^{L} ∈ L_{y} : x ≤ y^{L},
(3) x > y ⟺ x ≥ y and x ▷ y,
(4) x = y ⟺ x ≥ y and y ≥ x,
(5) x ∥ y ⟺ x ▷ y and y ▷ x.

Proof:

(1): x ≤ y ⟺ ∀ (x − y)^{L} ∈ L_{x−y} : (x − y)^{L} ◁ 0
⟺ ∀ x^{L} ∈ L_{x} : x^{L} − y ◁ 0 and ∀ y^{R} ∈ R_{y} : x − y^{R} ◁ 0.

(2) is proved similarly, while (3), (4) and (5) are plain. □ 4.4 Note. (Properties of order) For all games x, y, z ∈ Ug_{⋆} the following statements hold.

\begin{matrix}(1) & x ≥ x, \\ (2) & x ≥ y and y ≥ z ⟹ x ≥ z, \\ (3) & x ≥ y and y ▷ z ⟹ x ▷ z, \end{matrix}

(4) x ≥ y ⟺ x + z ≥ y + z,
(5) x ▷ y ⟺ x + z ▷ y + z,
(6) x^{L} ◁ x and x ◁ x^{R} whenever x^{L} ∈ L_{x}, x^{R} ∈ R_{x}.

(For (1) and (6) use 3.6 (4), for (2), (3), (4) and (5) use 2.6.)

4.5 Remark. (Properties of strict order) For all games x, y, z ∈ Ug_{⋆} we have

\begin{matrix}(1) & ¬(x > x), \\ (2) & x > y ⟹ ¬(y > x), \\ (3) & x > y and y > z ⟹ x > z, \\ (4) & x > y ⟺ x + z > y + z. \end{matrix}

((1) and (2) are proved with 1.9 (1); (3) and (4) are consequences of 4.4.)

4.6 Result. ≥ is a preorder relation (reflexive and transitive) on Ug_{⋆} with associated equivalence relation =, and > is a strict partial order relation on Ug_{⋆}.

5. EQUALITY

5.1 Note. The equivalence relation = (cf. 4.1 and 4.6) is invariant with respect to translations and reflections, i. e. for all x, y, z ∈ Ug_{⋆}

\begin{aligned}(1) & x = y & ⟹ & x + z = y + z, \\ (2) & x = y & ⟹ & −x = −y. \end{aligned}

(The proofs are straightforward with 4.3 (4), 4.4 and 3.5.)

5.2 Observation. Addition and subtraction preserve equality, and ≥, ▷, > as well as ∥ allow substitution of equals, viz. for all x_{1}, x_{2}, y_{1}, y_{2}, x, y, z ∈ Ug_{⋆} the following statements hold.

\begin{aligned}(1) & x_{1} = x_{2} and y_{1} = y_{2} & ⟹ x_{1} + y_{1} = x_{2} + y_{2}, \\ (2) & x_{1} = x_{2} and y_{1} = y_{2} & ⟹ x_{1} − y_{1} = x_{2} − y_{2}, \end{aligned}

(3) x = y and y ϱ z ⟹ x ϱ z whenever ϱ ∈ {≥, ▷, >, ∥},
(4) x ϱ y and y = z ⟹ x ϱ z whenever ϱ ∈ {≥, ▷, >, ∥}.

((1) and (2) are consequences of 5.1, the proofs of (3) and (4) for ≥ and ▷ are plain with 4.4, then (3) and (4) for > and ∥ follow easily .)

5.3 Result. Ug_{⋆}, i. e. Ug_{⋆} modulo = , is a partially ordered group. (Here bold print symbolizes the employment of = as equality.)

5.4 Lemma. Let x, y ∈ Ug_{⋆} and L′, R′ ⊆ G_{α} with α ∈ On_{j}, j ∈ ℕ_{0}. Then

(1)  (L_{x} ∪ L′, R_{x}) = x, if L′ ◁ x (i. e. if x′ ◁ x for all x′ ∈ L′);
(2)  (L_{y}, R_{y} ∪ R′) = y, if y ◁ R′ (i. e. if y ◁ y′ for all y′ ∈ R′);
(3) (L_{x} ∪ L′, R_{x} ∪ R′) = x, if L′ ◁ x ◁ R′

(i. e. if x′ ◁ x ◁ y′ for all x′ ∈ L′, y′ ∈ R′).

Proof: In (1) let x̃ ≡ (L_{x} ∪ L′, R_{x}) and prove x̃ ≤ x: We have L′ ◁ x by assumption and L_{x} ◁ x by 4.4 (6), hence Lx̃ = (L_{x} ∪ L′) ◁ x. Moreover, by 4.4 (6), we have x̃ ◁ Rx̃ = R_{x}. (x ≤ x̃ is proved similarly.) For (2) apply (1) with x = −y, L′ = −R′, for (3) apply (1) and (2). □

5.5 Notation. For every subset A ⊆ X of a set X with preorder ≤ we call

↑A:= { x ∈ X : ∃ a ∈ A : a ≤ x } the upwards closure of A,
↓A:= { x ∈ X : ∃ a ∈ A : x ≤ a } the downwards closure of A.

5.6 Hint. ↑ and ↓ are closure operators:

(1) A ⊆ ↑A and A ⊆ ↓A,
(2) ↑↑A = ↑A and ↓↓A = ↓A,
(3) A ⊆ B ⟹ ↑A ⊆ ↑B and ↓A ⊆ ↓B,
(4) (A ⊆ ↑B ⟺ ↑A ⊆ ↑B) and (A ⊆ ↓B ⟺ ↓A ⊆ ↓B).

(The proofs are plain; closure spaces are presented in [5].)

5.7 Proposition. For all games x, y ∈ Ug_{⋆} the following statements hold.

(1) L_{x} ⊆ ↓L_{y} and R_{y} ⊆ ↑R_{x} ⟹ x ≤ y,
(2) ↓L_{x} = ↓L_{y} and ↑R_{y} = ↑R_{x} ⟹ x = y.

(The implications are no equivalences; for instance, x ≡ {∗|} = {|} ≡ y by 5.4 as ∗ ≡ {⊥|⊥} ◁ ⊥ ≡ {|}, but L_{x} = {∗} ⊋ ∅ = ↓L_{y}.)

Proof: (1): Because of L_{x} ⊆ ↓L_{y} we have L_{x} ◁ y (i. e. x^{L} ◁ y for all x^{L} ∈ L_{x}) and because of R_{y} ⊆↑R_{x} we have x ◁ R_{y} (i. e. x ◁ y^{R} for all y^{R} ∈ R_{y}).

(2) is a consequence of (1). □

5.8 Interpretation. Proposition 5.7 (2) is interpreted as follows: To omit any dominated option leaves the value of a game unchanged. (A dominated option of x is a Left option x^{L} ∈ ↓(L_{x} ∖ {x^{L}}) or a Right option x^{R} ∈ ↑(R_{x} ∖ {x^{R}}).)

6. CONWAY NUMBERS

6.1 Motivation. The difference x^{L}−x (resp. x−x^{R}) is the so-called incentive for a move from x to x^{L} (resp. from x to x^{R}), cf. [2] p. 207. If x^{L} < x (resp. x^{R} > x) does always hold, Left (resp. Right) will try to avoid moving in x because every move would be disadvantageous. (High/low values are advantageous for Left resp. Right.) A game z ∈ Ug_{⋆} with this negative incentive property, in which in addition all (Left and Right) options also have this same property, is called Conway number.

6.2 Definition. (Conway numbers) A Conway number is a Conway game z ∈ Ug_{⋆} satisfying the following conditions:

(N1) z^{L} ◁ z^{R} for all z^{L} ∈ L_{z}, z^{R} ∈ R_{z},
(N2) all z^{L} ∈ L_{z} and all z^{R} ∈ R_{z} are Conway numbers.

Analogously to 1.2 define sets N_{α} ⊂ G_{α} for every α ∈ On_{j}, j ∈ ℕ_{0}: N_{0} := G_{0}, N_{1} := { z ∈ Γ(N_{0}) : (N1) } , N_{2} := { z ∈ Γ(N_{1}) : (N1) } , … N_{ω} := { z ∈ Γ (⋃_{k=0}^{∞} G_{k}) : (N1) } , N_{ω+1} := { z ∈ Γ(G_{ω}) : (N1) }, etc.

No_{j} := ⋃ { N_{α} : α ∈ On_{j} } may be called the j-th Conway number class (j ∈ ℕ_{0}), and No_{⋆} := ⋃_{j=0}^{∞} No_{j} is the set of all Conway numbers. (Conway denotes by No his proper class of numbers, cf. [2] p. 4.)

6.3 Examples. (M, ∅) and (∅, M) are Conway numbers for any set of Conway numbers M ⊂ N_{α} (α ∈ On_{j}, j ∈ ℕ_{0}). Especially ⊥ ≡ {|}, 1_{L} ≡ {⊥|} and 1_{R} ≡ {|⊥} are Conway numbers.

∗ ≡ {⊥|⊥} is not a Conway number as ⊥ ◁ ⊥ does not hold.

6.4 Remark. (Properties of Conway numbers) For all Conway numbers z, z_{1}, z_{2} ∈ No_{⋆} we have

(1) z^{L} < z < z^{R} whenever z^{L} ∈ L_{z}, z^{R} ∈ R_{z};
(2) z_{1} ◁ z_{2} ⟺ z_{1} < z_{2};
(3) −z, z_{1} + z_{2} ∈ No_{⋆}.

Therefore No_{⋆}, i. e. No_{⋆} modulo = , is a subgroup of Ug_{⋆}. ( (1) is proved using (N1) and 4.4 (3) by Conway number induction, i. e. by transfinite induction on α ∈ On_{j}, j ∈ ℕ_{0}, z ∈ N_{α}; using 4.3 (2) and 4.4 we obtain (2) from (1); now (3) is proved with ((2) by game inductions.)

6.5 Lemma. (Simplicity Lemma) Let x ∈ Ug_{⋆} be a game. Then x = z for any number z ∈ No_{⋆} with L_{x} ◁ z ◁ R_{x} (i. e. with x^{L} ◁ z ◁ x^{R} for all x^{L} ∈ L_{x}, x^{R} ∈ R_{x}), L_{z} ⊆ ↓L_{x} and R_{z} ⊆ ↑R_{x}. (If the assumptions hold, z is the “simplest” Conway number between L_{x} and R_{x}, because – as z^{L} ≤ x^{L} and x^{R} ≤ z^{R} hold for some x^{L} ∈ L_{x} and x^{R} ∈ R_{x} – it is impossible that always x^{L} ◁ z^{L} ◁ x^{R} or x^{L} ◁ z^{R} ◁ x^{R}.)

Proof: z ≤ x: Because of L_{z} ⊆↓L_{x} we have L_{z} ◁ x (i. e. z^{L} ◁ x for all z^{L} ∈ L_{z}), and by assumption we have z ◁ R_{x}. (x ≤ z is proved similarly.) □

6.6 Auxiliary Theorem. (Dyadic Conway numbers) Set D_{k} := 2^{−k}ℤ for all k ∈ ℕ_{0}, and let D_{∞} := ⋃_{k=0}^{∞} D_{k} denote the set of dyadic rationals (i. e. rationals \frac{m}{2^{k}} with m ∈ ℤ, k ∈ ℕ_{0}).

(1) There is a unique map c_{∞} : D_{∞} → No_{⋆} with image c_{∞}[D_{∞}] ⊆ No_{1} and (i) c_{∞}(0) ≡ \{|\} ≡ ⊥, the neutral element of No_{⋆}, (ii) c_{∞}(n) ≡ \{c_{∞}(n − 1)|\} for all n ∈ ℕ, (iii) c_{∞}(−n) ≡ \{|−c_{∞}(n − 1)\} for all n ∈ ℕ, (iv) c_{∞}(\frac{2ℓ+1}{2^{k}}) ≡ \{c_{∞}(\frac{ℓ}{2^{k−1}} ) |c_{∞}(\frac{ℓ+1}{2^{k−1}} )\} for all k ∈ ℕ, ℓ ∈ ℤ.

(2) c_{∞} is reflection preserving and strictly increasing, i. e. we have c_{∞}(−s) ≡ −c_{∞}(s) and c_{∞}(s) < c_{∞}(t) if s < t and s, t ∈ D_{∞}.

(3) \overline{c}_{∞} := \overline{pr}∘c_{∞} is an injective group homomorphism \overline{c}_{∞} : D_{∞} → No_{⋆}, where \overline{pr} : No_{⋆} → No_{⋆} is the canonical projection (No_{⋆} as in 6.4).

Proof: (1): First construct c_{0} : ℤ → No_{⋆} satisfying c_{0}[ℤ] ⊂ No_{1} as well as (i), (ii) and (iii) with c_{0} instead of c_{∞}, then extend c_{k−1} : D_{k−1} → No_{⋆} to c_{k} : D_{k} → No_{⋆} using (iv) with c_{k} instead of c_{∞}. Finally define c_{∞}(s) to be c_{k}(s) if s ∈ D_{k}. Uniqueness is proved by inductions on n and on k.

(2) is proved with (1) (i)–(iv), and (3) is proved with 6.5. □

6.7 Convention. Dyadic rationals can be interpreted as Conway numbers by dint of 6.6. Numbers of the form c_{∞}(s) with s ∈ D_{∞} may be called dyadic Conway numbers. Occurrences of c_{∞} will usually be suppressed, provided that no misunderstandings are to be expected: 0 ≡ \{|\}, 1 ≡ \{0|\}, 2 ≡ \{1|\}, 3 ≡ \{2|\}, …, \frac{1}{2} ≡ \{0|1\}, \frac{1}{4} ≡ \{0| \frac{1}{2}\}, \frac{3}{4} ≡ \{\frac{1}{2} |1\}, −1 ≡ \{|0\}, −2 ≡ \{|−1\}, −3 ≡ \{|−2\}, …, −\frac{1}{2} ≡ \{−1|0\}, −\frac{1}{4} ≡ \{−\frac{1}{2} |0\} etc. (Writing 0 for ⊥ is consistent with Definition 1.6, as xϱ⊥ is equivalent to xϱ 0 for every ϱ ∈ {≥, ▷, ≤, ◁, >, <, ∥, =}; in 1.4 we have 1_{L} ≡ 1 and 1_{R} ≡ −1.)

7. REAL CONWAY NUMBERS

7.1 Definition. (Real Conway numbers) A Conway number z ∈ No_{⋆} is called real if

(R1) −n < z < n for some n ∈ ℕ,
(R2) for all z^{L} ∈ L_{z} there is an m ∈ ℕ with z − z^{L} > 2^{−m}

and for all z^{R} ∈ R_{x} there is an m ∈ ℕ with z^{R} − z > 2^{−m}.

We call a (real) Conway number z located if c(s) < z or z < c(t) holds whenever s, t ∈ D_{∞} with s < t. We set No_{real} := { z ∈ No_{⋆} : z is real } and R := \overline{pr} [\{ z ∈ No_{real} : z is located \}] (with \overline{pr} from 6.6).

7.2 Example. Dyadic Conway numbers (cf. 6.7) are located reals.

7.3 Remark. (Properties of real Conway numbers)

(1) R is a subgroup of No_{⋆}.
(2) A real Conway number z is located if and only if for every k ∈ ℕ
there are s, t ∈ D_{∞} with z − 2^{−k} < s < z < t < z + 2^{−k}.
(3) For z_{1}, z_{2} ∈ No_{real} with z_{1} < z_{2} there is m ∈ ℕ with z_{2} − z_{1} > 2^{−m}.

7.4 Auxiliary Theorem. (Rational Conway numbers)

(1) c : ℚ → No_{⋆}, q ↦ (c_{∞}[{ s ∈ D_{∞} : s < q }], c_{∞}[{ s ∈ D_{∞} : s > q }])

satisfies c(s) = c_{∞}(s) for all s ∈ D_{∞} (with c_{∞} and D_{∞} from 6.6).

(2) All rational Conway numbers (elements of c[ℚ]) are located reals.
(3) c is reflection preserving and strictly increasing, i. e. we have

c(−q) ≡ −c(q) and c(p) < c(q) if p < q and p, q ∈ ℚ.

(4) \overline{c} := \overline{pr} ∘ c is an injective group homomorphism \overline{c} : ℚ → No_{⋆}

with image Q := \overline{c}[ℚ] ⊂ R (where \overline{pr} : No_{⋆} → No_{⋆} is as in 6.6).

(5) The following statements is equivalent to (LEM) from 1.9:

(a) Every z ∈ R can be approximated on both sides by rational numbers, i. e. for all z ∈ R and all k ∈ ℕ there are r_{1}, r_{2} ∈ Q with z − 2^{−k} < r_{1} < z < r_{2} < z + 2^{−k}.

(b) All Conway reals are located.

Proof: (1),(2): c(q) is a located real Conway number because c_{∞} is strictly increasing, while c(s) = c_{∞}(s) can be seen with 5.4.

(3) is proved easily using the definition of c, and (4) is proved with 6.5. (5): “(a) ⟺ (b)” is proved with 7.3, “(LEM) ⟹ (b)” with 1.9 (2), and for “(b) ⟹ (LEM)” use the real Conway number z_{ψ} ≡ −x_{ψ} with x_{ψ} as in the proof of 1.9. □

7.5 Definition. (Rational cuts) A rational cut is a pair (P, Q) of subsets P, Q ⊆ ℚ such that

(C1) P and Q are downwards/upwards closed: ↓P = P and ↑Q = Q,
i. e. p < p′ ∈ P ⟹ p ∈ P resp. q > q′ ∈ Q ⟹ q ∈ Q;
(C2) P and Q are disjoint, thus P < Q, (p < q for all p ∈ P, q ∈ Q;)
(C3) P and Q are open, i. e. for all p ∈ P there is p′ ∈ P with p′ > p
and for all q ∈ Q there is q′ ∈ Q with q′ < q.

A rational cut (P, Q) is called bounded if P and Q are non-empty, and (P, Q) is called located if P ∪ Q is dense in ℚ (equivalently p ∈ P or q ∈ Q whenever p, q ∈ ℚ with p < q).

7.6 Theorem. (Real Conway numbers and rational cuts)

(1) For all rational cuts (P, Q) the Conway number ĉ(P, Q) ≡ (c[P], c[Q]) satisfies (R2); it is real (and located) if (P, Q) is bounded (and located).

(2) For every real Conway number z the rational cut č(z) := (P_{z}, Q_{z}) with P_{z} := { p ∈ ℚ : c(p) < z } and Q_{z} := { q ∈ ℚ : c(q) > z } is located if z is located. Whenever (P, Q) is located we have č(ĉ(P, Q)) = (P, Q).

(3) There is a bijection between the set R (defined in 7.1) and the set ℝ of Dedekind reals, i. e. bounded and located rational cuts.

Proof: (1) is proved straightforwardly. (2): The assertions of the first sentence are easily verified; s < ĉ(P, Q) can hold with a located rational cut (P, Q) only if s ∈ P. (3): Using 7.3 (1) we have L_{z} ⊆ ↓c[P_{z}], R_{z} ⊆ ↑c[Q_{z}] for z ∈ R, thus z = ĉ(č(z)) holds by the Simplicity Lemma 6.5, as c[P_{z}] < z < c[Q_{z}]. □

8. GENERALIZED REAL NUMBERS

Generalized Dedekind reals (introduced by Fred Richman in [6] and Peter Schuster in [9]) are just rational cuts (cf. 7.5). Addition for these cuts is defined by (P, Q) + (P′, Q′) := (P + P′, Q + Q′) in contrast to 2.2, whereas reflection −(P, Q) := (−Q, −P) corresponds to Definition 3.2. The partial order relation for cuts defined by (P, Q) ≤ (P′, Q′) :⟺ (P ⊆ P′ and Q ⊇ Q′) is different from the one defined in 4.1, because all cuts of the form (P, Q) = (ℚ ∖ ↑{p}, ℚ ∖ ↓{q}), with ↑and ↓from 5.5, have ĉ(P, Q) = 0 if p < 0 < q. In [6] multiplication is defined only for weakly positive cuts (i. e. for cuts with (P, Q) ≥ 0). Conway’s definition of multiplication (cf. [2] p. 19)

xy ≡ {x^{L}y + xy^{L} − x^{L}y^{L},x^{R}y + xy^{R} − x^{R}y^{R} |

x^{L}y + xy^{R} − x^{L}y^{R}, x^{R}y + xy^{L} − x^{R}y^{L}}

is possibly useful to define a product for arbitrary cuts.

Acknowledgments

I am grateful to Peter Schuster for drawing my attention to the Symposion “Reuniting the Antipodes” and to Conway’s article [3], for several preprints of [9] as well as for encouraging me to give a talk on Conway numbers in Venice. Volkswagen foundation Hannover and FernUniversität Hagen supported my participation at the Symposion “Reuniting the Antipodes” in May 1999 at Venice International University. Furthermore I appreciate the valuable instructions of Prof. Holger P. Petersson before my departure and after my return to FernUniversität Hagen, and the helpful discussions with participants of the “Oberseminar über Algebra und Topologie”, where I presented some details of constructive Conway theory in June 1999. Moreover I want to thank Dipl. Math. Peter Brühne and HDoz. Goswin Große-Erdmann for proof-reading penultimate versions of this paper as well as Prof. Reinhard Börger for discussing some technical items. Their notes, suggestions and hints turned out to be very helpful during the revision.

The anonymous referee stimulated the revised version of this paper by insisting on precision concerning the employed notion of ordinal numbers, a topic I discussed in November 1999 with Per Martin-Löf in Munich. I am indebted to both of them for giving me a fresh impetus to improve the performance and to write [8], an extended version of my talk given in Hagen.

This paper is dedicated to my wife Monika Rosemeier and to our newborn daughter Lena Tabea. Thanks to their patience I could finish the revisions of it in time. Let us appreciate the indispensable value of playing for the development of human life.

References

[1] Elwyn R. Berlekamp, John H. Conway, Richard K. Guy: Winning Ways, Academic Press, London, GB, 1982, 3rd ed. 1985.

[2] John H. Conway: On Numbers and Games, Academic Press, London, GB, 1976.

[3] John H. Conway: The surreals and the reals, in [4] 93–103.

[4] Philip Ehrlich (ed.): Real Numbers, Generalizations of the reals and Theories of Continua, Kluwer, Dordrecht, NL, 1994.

[5] Norman M. Martin, Stephen Pollard: Closure Spaces and Logic, Kluwer, Dordrecht, NL, 1996.

[6] Fred Richman: Generalized Real Numbers in Constructive Mathematics, Indag. Mathem., N. S., 9 (4) (1998) 595–606.

[7] Fred Richman: The fundamental theorem of algebra: a constructive development without choice, to appear in Pacific J. Math.

   http://www.math.fau.edu/Richman/html/docs.htm

[8] Frank Rosemeier: A Constructive Approach to Conway’s Theory of Games, to appear in Seminarberichte aus dem Fachbereich Mathematik, FernUniversität Hagen (ISSN 0944-5838).

   http://www.fernuni-hagen.de/MATHEMATIK/ALGGEO/
   Mitarbeiter/Rosemeier/publ.html

[9] Peter Schuster: A Constructive Look at Generalised Cauchy Reals, Math. Logic Quaterly 46 no. 1 (2000) 125-134.