A Constructive Approach to Conway’s Theory of Games ^{∗}

Frank Rosemeier ^{∗∗}

Abstract. John H. Conway presents in his book “On Numbers and Games” [ONAG] 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 [ONAG] 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. A constructive approach to ordinal numbers which is compatible with constructive Conway theory is presented. Key words. Constructive mathematics, Conway games, Conway numbers, ordinal numbers.

Introduction

In his book “On Numbers and Games” ([ONAG]=[11]) John Horton 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 the ideas of Conway, 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 in his talk at the Symposion “Reuniting the Antipodes”, cf. [1]; cf. also [23] and [25].)

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. Conway numbers are dealt with in Section 6, and real Conway numbers are the topic of Section 7.

∗ Mathematics Subject Classification 2000. 03F65 (03F15, 03H15, 91A05)

∗∗ The author presented the ideas of this paper for the first time at the Symposion “Reuniting the Antipodes” in May 1999 at Venice International University, cf. [1]. His participation has been supported by Volkswagen foundation Hannover and by FernUniversität Hagen.

(First version July 1999, intermediate versions February, April and July 2000, final version October 2000.)

Constructive background material about ordinal numbers, their order and addition is sketched in Appendix A resp. B.

Zeroth Part On Games …

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 Appendix A, where a constructive notion of ordinal numbers is presented.)

Then Ug_{j} := ⋃ { G_{α} : α ∈ On_{j} } may be called j-th (Conway) game class (j ∈ ℕ_{0}), and elements of the set Ug_{⋆} := ⋃ { G_{α} : α ∈ On_{⋆} } = ⋃_{j=0}^{∞} Ug_{j} are (Conway) games. (Conway took the name Ug to denote his proper class of all “unimpartial” games, i. e. games possibly favouring one of the players, cf. [ONAG]=[11] p. 78. The sets On_{j} and On_{⋆} are defined in A.2 resp. A.7.)

1.3 Notation (Left/Right Options) With the projections pr_{L} : Ug_{⋆} ⟶ Ug_{⋆}, (L, R) ⟼ L and pr_{R} : Ug_{⋆} ⟶ Ug_{⋆}, (L, R)⟼R we obtain two sets of games for every game x ∈ Ug_{⋆}: L_{x} := pr_{L}(x), the set of Left options in x, and R_{x} := pr_{R}(x), the set of 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). {x_{1}, …, x_{n}|y_{1}, …, y_{m}} will 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}. The following games are elements of Ug_{1}:

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

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

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

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

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’. Relying on this intuitive concept, some readers may prefer to define the outcome classes by the expresssions in parentheses. They can arrive at the formal definition given here by considering remark 1.7. Other readers may use the formal definitions given here to make precise the concept of winning strategy using remark 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. The outcome classes in favour of Right (x ≤ 0 and x ◁ 0) can be interpreted similarly.

1.8 Examples Here are 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): The proofs of (i) and (ii) are carried out by mutual game induction, i. e. by game induction (transfinite induction on α ∈ On_{⋆}, 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 analogously 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_{ψ} ≡ (∅, { x ∈ {⊥} : ψ }) ∈ Ug_{⋆}. Then with R_{ψ} := { x ∈ {⊥} : ψ } we have

\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_{⋆} can be 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 of the sum x + y of two games.

2.2 Definition (Addition) For games x, y ∈ Ug_{⋆} their (disjunctive) sum is given by 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} } and R_{x+y} := (R_{x} + y) ∪ (x + R_{y}) = { x^{R} + y : x^{R} ∈ R_{x} } ∪ { x + y^{R} : y^{R} ∈ R_{y} }. Or, using a more condensed notation, x+y ≡ {x^{L} + y, x + y^{L}|x^{R} + y, x + y^{R}}.

2.3 Remark For all α, β ∈ On_{j}, j ∈ ℕ_{0}, there is γ ∈ On_{j} with x + y ∈ G_{γ} for all x ∈ G_{α} and y ∈ G_{β}. The function add_{Ug_{⋆}} : Ug_{⋆}×Ug_{⋆}⟶Ug_{⋆}, (x, y)⟼x+y satisfies add_{Ug_{⋆}}(x, y) ∈ Ug_{j} whenever 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.

(1)  x ≥ 0 and y ≥ 0 ⟹ x + y ≥ 0,
(2)  x ≥ 0 and y ▷ 0 ⟹ x + y ▷ 0,
(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.

(A game theoretic interpretation of some of these implications is given in 2.7.)

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} ∈ L_{x} : 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. The third implication of 2.6 says that Left can win a game x if Right starts, provided Left can win a sum x + y if Right starts, where y is a game which can be won by Right having the second move. Indeed, Right may choose to move in x and, as y ≤ 0, every reply of Left in y can be countered by Right with a good move. Thus, Left can win the sum x + y only by finding a winning move in the game x. The remaining implications of 2.6 can be interpreted in an analogous manner.

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} }. Or, using a more condensed notation, −x ≡ {−x^{R}|−x^{L}}. The difference of x, y ∈ Ug_{⋆} is defined to be

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}, so using add_{Ug_{⋆}} from 2.3 we obtain a function sub_{Ug_{⋆}} : Ug_{⋆} × Ug_{⋆} ⟶ Ug_{⋆}, (x, y) ⟼ x − y satisfying sub_{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 together with (3) and 3.5 (1) yields x − x ≥ 0.) Because of x^{L} − x^{L} ≤ 0 [Ind. Hyp.] we have x^{L} − x ◁ 0 for all x^{L} ∈ L_{x}, and because of x^{R} − x^{R} ≤ 0 [Ind. Hyp.] we have x − x^{R} ◁ 0 for all x^{R} ∈ R_{x}. 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.

(1) x ≥ x,
(2) x ≥ y and y ≥ z ⟹ x ≥ z,
(3) x ≥ y and y ▷ z ⟹ x ▷ z,
(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), while (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, that is to say that for all x, y, z ∈ Ug_{⋆} we have

\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.)

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

5.4 Lemma Let x, y ∈ Ug_{⋆} be games and let L′, R′ ⊆ G_{α} be sets of games, α ∈ On_{⋆}. 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 and L′ = −R′, for (3) apply (1) and (2). □

5.5 Notation For every subset A ⊆ X of any 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 [17].)

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.

(It is not possible to replace the implications by 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) can be interpreted as follows: The omission of 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}}).)

First Part … and Numbers

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. [ONAG]=[11] 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 values are advantageous for Left, while low values are advantageous for 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_{⋆}:

N_{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.

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

6.3 Examples (M, ∅) and (∅, M) are Conway numbers for any set of Conway numbers M ⊂ N_{α} (α ∈ On_{⋆}). 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_{⋆}, z ∈ N_{α}; with 4.3 (2) and 4.4 we obtain (2) as consequence of (1) , and (3) is proved using (2) by Conway 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 x^{L} ◁ z^{L} ◁ x^{R} or x^{L} ◁ z^{R} ◁ x^{R} can always hold.)

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}). Then the following statements hold.

(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_{∞} defines an injective group homomorphism \overline{c}_{∞} : D_{∞} ⟶ No_{⋆}, where \overline{pr} : No_{⋆} ⟶ No_{⋆} is the canonical projection (with 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 every map c_{k−1} : D_{k−1} ⟶ No_{⋆} to a map 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 using the identities from (1), while (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, e. g. 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 it satisfies the following conditions:

(R1) −n < z < n for some n ∈ ℕ, and
(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. In addition 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 All 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 all z_{1}, z_{2} ∈ No_{real} with z_{1} < z_{2} there is an 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_{∞} (where c_{∞} and D_{∞} are as in 6.6).

(2) All rational Conway numbers (i. e. 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 defines an injective group homomorphism \overline{c} : ℚ ⟶ No_{⋆} with image Q := \overline{c}[ℚ] ⊂ R (where \overline{pr} : No_{⋆} ⟶ No_{⋆} is as in 6.6).

(5) Each of 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 using the definition of c, and (4) is proved with 6.5. (5): “(a) ⟺ (b)” is proved with 7.3, “(LEM) ⟹ (b)” follows from 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 resp. 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, i. e. p < q for all p ∈ P, q ∈ Q;
(C3) P and Q are open, i. e. for every p ∈ P there is a p′ ∈ P with p′ > p

and for every q ∈ Q there is a 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 every rational cut (P, Q) there is a Conway number ĉ(P, Q) ≡ (c[P], c[Q]) satisfying (R2), which is real (and located) if (P, Q) is bounded (and located).

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

(3) There is a bijection between R, defined in 7.1 to be the set of located Conway reals modulo = , 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 verified easily, and s < ĉ(P, Q) can hold with a located rational cut (P, Q) only if s ∈ P. (3): For located reals we have L_{z} ⊆ ↓c[P_{z}], R_{z} ⊆ ↑c[Q_{z}] using 7.3 (1), thus z = ĉ(č(z)) holds by the Simplicity Lemma 6.5, as clearly c[P_{z}] < z < c[Q_{z}]. □

Appendix On Ordinals

A Ordinal Numbers

A.1 Motivation In [8] Georg Cantor constructed for any point set P a sequence of derived sets P′, P′′, …; in [9] he generalized this construction and obtained a sequence P′, P′′, …, P^{(∞)}, P^{(∞+1)}, P^{(∞+2)}, … containing derived sets of infinite orders. The generalized numbers appearing here as orders of derived sets were called ordinal numbers (“Ordnungszahlen”) by Cantor. In [10] he defined sums and products for these numbers and wrote ω instead of ∞.

In the twentieth century other authors dealt with ordinal numbers as wellordered sets, e. g. Luitzen E. J. Brouwer in [7] and John von Neumann in [20]. This approach is nowadays preferred and leads to a proper class On, the collection of all ordinal numbers, cf. e. g. [21]. For the Conway theory presented in this paper it is sufficient to use a set On_{⋆} of ordinal numbers (defined in A.7) instead of the proper class On.

The following definition adapts the notion of ordinal numbers given by Per Martin-Löf in [18] p. 79ff and generalizes his definition of the second number class. (W-types are not used.)

A.2 Definition (Ordinal numbers) For every natural number j ∈ ℕ_{0} define recursively a set On_{j} satisfying the following conditions. (The set On_{j} may be called j-th ordinal number class.)

(i) 0 ∈ On_{j}; (ii) for any i ∈ {0, …, j − 1} and every function l : On_{i} ⟶ On_{j} there is an element Suc_{i}^{j}(l) in On_{j}; (iii) every element of On_{j} is constructed by (i) and (ii) in a finite number of steps. (For the functions l in (ii) extensionality, i. e. α = β ⟹ l(α) = l(β), is out of question, because up to now we have not defined any equality relation on On_{j}; such a definition will be given in B.2. Some readers might like to replace “function” by “operation” in (ii) as well as in the whole appendix, understanding an operation to be a “nonextensional function”, cf. [5] p. 15. Here the notion of operation is taken to be primitive, it cannot be reduced to that of an extensional function with multiple values as proposed in [19] p. 30f and included in [6] p. 54. Similarly, it is possible to put “preset” instead of “set” throughout the appendix, understanding a preset to be a “set without equality”, cf. [3] p. 34f.)

A.3 Hint We may say that elements of the form Suc_{i}^{j}(l) contain each l(α) (α ∈ On_{i}, l : On_{i} ⟶ On_{j}, i ∈ {0, …, j − 1}, j ∈ ℕ_{0}).

On_{j} satisfies a Descending Chain Condition with respect to this relation of containment (denoted by ≺): Because of A.2 (iii) there is no infinite sequence (α_{n})_{n∈ℕ} with α_{n} ∈ On_{j} and α_{n+1} ≺ α_{n} for all n ∈ ℕ.

A.4 Observation The following Principle of Transfinite Induction holds due to the inductive definition of the sets On_{j}. To prove a proposition ψ(α) for all α ∈On_{j} we must prove the Induction Basis ψ(0), and for each function l : On_{i} ⟶ On_{j} (i ∈ {0, …, j − 1}) we have to prove the Induction Step (∀ α∈On_{i} : ψ(l(α))) ⟹ ψ(Suc_{i}^{j}(l)).

We also have a form of Definition by Transfinite Recursion for functions with ordinal numbers as arguments. To define a function f : On_{j}⟶X from On_{j} to a set X, we must define f(0) ∈ X, and for each function l : On_{i} ⟶ On_{j} (i ∈ {0, …, j − 1}) we have to define f(Suc_{i}^{j}(l)) ∈ X, possibly using already defined values f(l(α)) ∈ X (α ∈ On_{i}).

A.5 Remark (Recursion operators) For ℕ_{0} there is a natural recursion operator “rec” with rec(x, f) : ℕ_{0} ⟶ X for any set X, x ∈ X and f : ℕ_{0} × X ⟶ X, such that rec(x, f)(0) = x and rec(x, f)(n + 1) = f(n, rec(x, f)(n)) for every n ∈ ℕ_{0}. The corresponding recursion operator for On_{1} is “rec_{1}” with rec_{1}(x_{0}, f_{0}) : On_{1} ⟶ X for any set X, x_{0} ∈ X and f_{0} : On_{1}^{On^{0}} × X^{On^{0}} ⟶ X, such that rec_{1}(x_{0}, f_{0})(0) = x_{0} and rec_{1}(x_{0}, f_{0})(Suc_{0}^{1}(l_{0})) = f_{0}(l_{0}, rec_{1}(x_{0}, f_{0}) ∘ l_{0}) for every l_{0} : On_{0} ⟶ On_{1}. Similarly, the recursion operator for On_{j} is “rec_{j}” (j ∈ ℕ_{0}) with

rec_{j}(x_{0}, f_{0}, f_{1}, …, f_{j−1}) : On_{j} ⟶ X for any set X, x_{0} ∈ X,

f_{i} : On_{j}^{On^{i}} × X^{On^{i}} ⟶ X (i ∈ {0, …, j − 1}),

such that rec_{j}(x_{0}, f_{0}, f_{1}, …, f_{j−1})(0) = x_{0} and

rec_{j}(x_{0}, f_{0}, f_{1}, …, f_{j−1})(Suc_{i}^{j}(l_{i})) = f_{i}(l_{i}, rec_{j}(x_{0}, f_{0}, f_{1}, …, f_{j−1}) ∘ l_{i})
for every l_{i} : On_{i} ⟶ On_{j} (i ∈ {0, …, j − 1}).

A.6 Note For any j, j′ ∈ ℕ_{0} with j < j′ we obtain by transfinite recursion (cf. A.4) a function h_{j j′} : On_{j} ⟶ On_{j′}, with 0 ⟼ 0 and Suc_{i}^{j}(l) ⟼ Suc_{i}^{j′}(h_{j j′} ∘ l) for every l : On_{i} ⟶ On_{j}, i < j. Similarly we obtain functions g_{j′j} : On_{j′} ⟶ On_{j} (j, j′ ∈ ℕ_{0}, j < j′) with 0 ⟼ 0, Suc_{i}^{j′}(l) ⟼ Suc_{i}^{j}(g_{j′j} ∘ l) whenever l : On_{i} ⟶ On_{j′}, i ∈ {0, …, j − 1}, and Suc_{i}^{j′}(l) ⟼ g_{j′j}(l(0)) whenever l : On_{i} ⟶ On_{j′}, i ∈ {j, …, j′ − 1}. (With respect to = as in B.2 these functions are not extensional in the sense of A.2.)

Because g_{j′j}(h_{j j′}(α)) is α for all α ∈ On_{j} (by transfinite recursion, cf. A.4), h_{j j′} is an embedding of On_{j} into On_{j′} for every j < j′.

A.7 Convention By dint of the functions h_{j j′} from A.6 we can interpret elements of On_{j} as elements of any On_{j′} with j′ > j, and we will write Suc_{i} instead of Suc_{i}^{i+1} as well as instead of Suc_{i}^{j} whenever the choice of j > i does not matter. Furthermore

we define On_{⋆} := ⋃_{j=0}^{∞} On_{j} ; elements of this set may be called ordinal numbers.

A.8 Notation Let l_{α} : On_{0} ⟶ On_{⋆}, x ⟼ α denote the constant function with value α ∈ On_{⋆}. Then we have a successor function suc : On_{⋆} ⟶ On_{⋆}, α ⟼ Suc_{0}(l_{α}). It is customary to distinguish three forms of ordinal numbers:

0. the zero ordinal 0,

1. successor ordinals of the form suc(α) with α ∈ On_{⋆},

2. lim-ordinals of the form Suc_{i}(l) with l : On_{i} ⟶ On_{j}, 0 < i < j. For lim-ordinals λ it is sometimes convenient to use a notation like lim_{α∈On_{i}} l(α) instead of Suc_{i}(l). Such a λ would be called limit ordinal if l is strictly increasing with respect to the relation < defined in B.2.

A.9 Examples

(0) The zero ordinal 0 is the only element of On_{0}.

(1) The elements of On_{⋆} constructed from 0 by applying the function suc a finite number of times may be called finite ordinal numbers. Let us denote suc(0) by 1, suc(1) by 2, suc(2) by 3, etc. Then we see that On_{1}, the set of all finite ordinal numbers, is just a disguised form of the set ℕ_{0} of natural numbers. (Even though On_{1} has infinitely many elements, the set On_{1} is finitely presented.)

(2) Because of (1), we can identify On_{1}-sequences with ordinary sequences. Let ω denote Suc_{1}(0, 1, 2, …), i. e. ω is Suc_{1}(h_{12}) ∈ On_{2} with h_{12} from A.6. (As h_{12} is rec_{1}(0, f_{0}) with f_{0}(l_{0}, l) := Suc_{1}^{2}(l) for l_{0} : On_{0} ⟶ On_{1}, l : On_{0} ⟶ On_{2} and rec_{1} as in A.5, the construction of ω requires only a finite number of steps.) Then we have a transfinite sequence 0, 1, 2, …, ω, suc(ω), suc(suc(ω)), … similar to Cantor’s sequence of derivational orders mentioned in A.1. By means of B.5 we will be able to write ω + 1 for suc(ω), ω + 2 for suc(suc(ω)), etc.

(3) More generally, let ω_{j−1} denote the ordinal number Suc_{j}(h_{j j+1}) for every j ∈ ℕ (with h_{j j+1} as defined in A.6). Then ω_{0} is ω, and for any j ∈ ℕ the element ω_{j−1} in On_{j+1} contains every element of On_{j}, i. e. α ≺ ω_{j−1} holds for all α ∈ On_{j} (if h_{j j+1}(α) is identified with α as in A.7; for ≺ cf. A.3).

B Ordinal order and ordinal addition

B.1 Motivation There is a function c_{⋆} : On_{⋆} ⟶ No_{⋆} which meets the following conditions.

(i) c_{⋆}(0) ≡ {|} ≡ ⊥, the neutral element of No_{⋆},
(ii) c_{⋆}(suc(α)) ≡ {c_{⋆}(α)|} for all α ∈ On_{⋆},
(iii) c_{⋆}(λ) ≡ (c_{⋆}[l[On_{i}]], ∅) for all lim-ordinals λ of the form Suc_{i}(l) with
l : On_{i} ⟶ On_{j}, 0 < i < j.

(Construct by transfinite recursion (cf. A.4) functions c_{j} : On_{j} ⟶ No_{⋆}, j ∈ ℕ_{0}, satisfying c_{j}[On_{j}] ⊂ No_{j} as well as (i), (ii) and (iii) with c_{j} instead of c_{⋆}. Then define c_{⋆}(α) to be c_{j}(α) if α ∈ On_{j}.)

By transfinite induction (cf. A.4) we have c_{⋆}(α) ∈ N_{α} for all α ∈ On_{⋆}, so c_{⋆}[On_{⋆}] ⊂ No_{⋆}. Conway numbers of the form c_{⋆}(α) with α ∈ On_{⋆} may be called Conway ordinals.

As L_{c_{⋆}(α)} = c_{⋆}[{ α′ ∈ On_{⋆} : α′ ≺ α }] (for ≺ see A.3) and R_{c_{⋆}(α)} = ∅ for all α ∈ On_{⋆}, characterization 4.3 (1),(2) might motivate Definition B.2. (Because of 6.4 (2) we write < instead of ◁.)

B.2 Definition (Ordinal order) For ordinal numbers α, β ∈ On_{⋆} define

α ≤ β :⟺ ∀ α′ ≺ α : α′ < β,  α ≥ β :⟺ β ≤ α,
α < β :⟺ ∃ β′ ≺ β : α ≤ β′,  α > β :⟺ β < α,
α = β :⟺ α ≤ β and β ≤ α.

B.3 Note For all ordinal numbers α, β ∈ On_{⋆} we have

\begin{matrix}(1) & 0 ≤ α and ¬(α < 0), \\ (2) & ¬(α ≤ β and α > β), \\ (3) & α ≤ α, \\ (4) & α ≺ β ⟹ α < β. \end{matrix}

(0 does not contain any ordinal number, so (1) is plain; (2) and (3) are easily proved by transfinite induction, and (4) is a consequence of (3).)

B.4 Lemma (Properties of ordinal order) For all ordinal numbers α, β, γ ∈ On_{⋆} the following statements hold.

(1) α ≤ β and β ≤ γ ⟹ α ≤ γ,
(2) α ≤ β and β < γ ⟹ α < γ,
(3) α < β and β ≤ γ ⟹ α < γ,
(4) α < β and β < γ ⟹ α < γ,
(5) α < β ⟹ α ≤ β.

Proof: (1), (2) and (3) are mutually proved by transfinite induction:

1) α′ ≺ α ≤ β ≤ γ ⟹ α′ < β ≤ γ [by B.3 (4) and Ind. Hyp. (3) ]
⟹ α′ < γ  [by Ind. Hyp. (3)].
2) α ≤ β ≤ γ′ ≺ γ ⟹ α ≤ γ′  [by Ind. Hyp. (1)].
3) α ≤ β′ ≺ β  ⟹ α ≤ β′ < γ [because β ≤ γ]
⟹ α < γ  [by Ind. Hyp. (2)].

(4) and (5) are mutually proved by transfinite induction:

4) α < β ≤ γ′ ≺ γ ⟹ α < γ′ [by (3)]
⟹ α ≤ γ′ [by Ind. Hyp. (5)].
5) α′ ≺ α < β  ⟹ α′ < β [by B.3 (4) and Ind. Hyp. (4)].

□

B.5 Definition (Ordinal addition) By transfinite recursion (cf. A.4) we define the sum of two ordinal numbers according to the form of the second summand (cf. e. g. Proposition 6.3.3 in [21])

α + 0 := α,
α + suc(β) := suc(α + β) for every β ∈ On_{⋆},
α + Suc_{i}(l) := lim_{γ∈On_{i}}(α + l(γ)) whenever l : On_{i} ⟶ On_{j}, 0 < i < j.

So we obtain a function add_{On_{⋆}} : On_{⋆} × On_{⋆} ⟶ On_{⋆}, (x, y) ⟼ x + y satisfying add_{On_{⋆}}(α, β) ∈ On_{j} whenever α, β ∈ On_{j}.

B.6 Examples

(1) Ordinal addition on On_{1} can be seen to be just the ordinary addition for natural numbers (cf. A.9 (1)).

(2) We have α < α + 1 for all α ∈ On_{⋆} and ν < ω for all ν ∈ On_{1}:

0 < 1 < 2 < … < ω < ω + 1 < ω + 2 < … (cf. A.9).

(3) Because of 1 + ω = ω < ω + 1, ordinal sums generally depend on the order of summation.

B.7 Proposition (Properties of ordinal addition) For all ordinal numbers α, β, γ ∈ On_{⋆} the following statements hold.

\begin{matrix}(1) & 0 + γ = γ, \\ (2) & α + (β + γ) = (α + β) + γ, \\ (3) & α ≤ β ⟹ α + γ ≤ β + γ, \\ (4) & α = β ⟹ α + γ = β + γ, \\ (5) & α + β ≤ α + γ ⟺ β ≤ γ, \\ (6) & α + β < α + γ ⟺ β < γ, \\ (7) & α + β = α + γ ⟺ β = γ. \end{matrix}

(Associativity of ordinal addition is well known since Cantor, cf. [10] p. 550f. As 0 + ω = 1 + ω, (3) with < instead of ≤ does not hold, and (5), (6) and (7) with reversed order of summation are not valid.)

Proof: (1), (2) and (3) are proved straightforwardly by transfinite inductions (on γ),

(4) is a consequence of (3); (5) and (6) are mutually proved by transfinite induction, and (7) is a consequence of (5). □

B.8 Result (On_{⋆} monoid) ≤ is a preorder relation (reflexive and transitive) on On_{⋆} with associated equivalence relation =, and < is a strict partial order relation on On_{⋆}. Thus On_{⋆} (i. e. On_{⋆} modulo =) with ordinal addition and ordinal order is an ordered monoid, having 0 as neutral element. In On_{⋆} the left cancellation law does hold, but On_{⋆} is not commutative.

B.9 Remarks

(1) The function c_{⋆} from B.1 is extensional (in the sense of A.2), injective and strictly increasing: We have c_{⋆}(α) ϱ c_{⋆}(β) ⟺ α ϱ β for all α, β ∈ On_{⋆} and for every ϱ ∈ {≤, <, =}. Furthermore c_{⋆} satisfies c_{⋆}(α + β) ≤ c_{⋆}(α) + c_{⋆}(β) for all α, β ∈ On_{⋆}; c_{⋆} is not a homomorphism, as this inequality is strict for α = 1, β = ω.

(2) A necessary and sufficient condition for On_{j+1} to be totally ordered, i. e. α ≤ β or α > β for all α, β ∈ On_{j+1}, is the j-th limited principle of omniscience (LPO_{j}) ∀ α ∈ On_{j} : l(α) = 0 or ∃ α ∈ On_{j} : l(α) = 1 for each l : On_{j}⟶{0, 1}. (If On_{1} is replaced by the set of natural numbers in (LPO_{1}) we obtain Bishop’s LPO as in [5] p. 3 or [19] p. 4. Because (LEM) implies (LPO_{j}) for any j ∈ ℕ_{0}, in classical mathematics On_{⋆} is totally ordered.)

First observe that (LPO_{j}) implies (LPO_{i}) for every i ∈ {0, …, j − 1}: For l : On_{i} ⟶ {0, 1} apply (LPO_{j}) to l ∘ g_{j i} with g_{j i} as in A.6.

Now prove sufficiency by transfinite induction on α: For α = Suc_{i}^{j+1}(l) with l : On_{i}⟶On_{j+1} and β ∈ On_{j+1} define l_{β} : On_{i}⟶{0, 1} with l_{β}(γ) = 0 if l(γ) < β and l_{β}(γ) = 1 if l(γ) ≥ β (this is possible by Ind. Hyp.). Apply (LPO_{i}) to l_{β}, then use α ≤ β ⟺ ∀ γ ∈ On_{i} : l_{β}(γ) = 0 and α > β ⟺ ∃ γ ∈ On_{i} : l_{β}(γ) = 1.

(LPO_{j}) is necessary because for every l : On_{j} ⟶On_{j+1} with l[On_{j}] ⊆ {0, 1} we have Suc_{j}(l) ≤ 1 ⟺ ∀ α ∈ On_{j} : l(α) < 1 ⟺ ∀ α ∈ On_{j} : l(α) = 0, and Suc_{j}(l) > 1 ⟺ ∃ α ∈ On_{j} : l(α) ≥ 1 ⟺ ∃ α ∈ On_{j} : l(α) = 1.

(3) It is possible to define ordinal multiplication by transfinite recursion in a manner similar to B.5 (cf. e. g. Proposition 6.4.3 in [21]).

Acknowledgements. I am grateful to Peter Schuster for drawing my attention to the Symposion “Reuniting the Antipodes” and to Conway’s article [12], for several preprints of [25] as well as for encouraging me to give a talk on Conway numbers in Venice. 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 Peter Brühne and Goswin Große-Erdmann for proofreading 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 revisions.

The anonymous referee of [24] stimulated the development 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. The criticism and the many questions of the referee were an incentive to make the appendix more comprehensive; he recommended the references [14], [15], [16] and [19] section I.6.

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

References

[1] Ulrich Berger, Horst Oswald, Peter Schuster (eds.): Reuniting the Antipodes, Constructive and Nonstandard Views of the Continuum, Proceedings of the Symposion in San Servolo/Venice, Italy, May 17–22, 1999. Forthcoming in the Synthèse Library by Kluwer Academic Publishers, Dordrecht, NL.

[2] Günter Asser (ed.), Georg Cantor: Über unendliche, lineare Punktmannigfaltigkeiten: Arbeiten zur Mengenlehre aus den Jahren 1872–1884, Teubner Verlagsgesellschaft, Leipzig, GDR, 1984.

[3] Michael J. Beeson: Foundations of Constructive Mathematics, Springer-Verlag, Berlin Heidelberg, D, 1985.

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

[5] Errett Bishop, Douglas Bridges: Constructive Analysis, Springer-Verlag, Berlin Heidelberg, D, 1985.

[6] Douglas Bridges, Fred Richman: Varieties of Constructive Mathematics, Cambridge University Press, Cambridge, GB, 1987.

[7] Luitzen E. J. Brouwer: Begündung der Mengenlehre unabhängig vom logischen Satz vom ausgeschlossenen Dritten, Verhandelingen der Koninklijke Akademie van Wetenschappen XII (5) 3–43, Johannes Müller, Amsterdam, NL, 1918.

[8] Georg Cantor: Über die Ausdehnung eines Satzes aus der Theorie der trigonometrischen Reihen, Math. Ann. 5 (1872) 123–132; in [2] 9–18.

[9] Georg Cantor: Über unendliche lineare Punktmannigfaltigkeiten, Teil 2, Math. Ann. 17 (1880) 355–358; in [2] 52–55.

[10] Georg Cantor: Über unendliche lineare Punktmannigfaltigkeiten, Teil 5, Math. Ann. 21 (1883) 545–591; in [2] 73–119.

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

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

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

[14] Robin J. Grayson: Constructive well-orderings, Z. Math. Logik Grundlag. Math. 28 (1982) 495–504.

[15] Leon Harkleroad: Recursive surreal numbers, Notre Dame J. Formal Logic 31 (1990) 337–345.

[16] Jacob Lurie: The effective content of surreal algebra, J. Symb. Logic 63 (1998) 337–371.

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

[18] Per Martin-Löf: Intuitionistic Type Theory, Bibliopolis, Napoli, I, 1984.

[19] Ray Mines, Fred Richman, Wim Ruitenburg: A Course in Constructive Algebra, Springer-Verlag, New York, NY, 1988.

[20] John von Neumann: Zur Einführung der transfiniten Zahlen, Acta litterarum ac scientiarum Regiae Universitatis 1 (1923) 199–208.

[21] Michael D. Potter: Sets, Clarendon Press, Oxford, GB, 1990.

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

[23] 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

[24] Frank Rosemeier: On Conway Numbers and Generalized Real Numbers, to appear in [1].

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

Frank Rosemeier FernUniversität Hagen D-58084 Hagen (Germany)

E-mail address: frank.rosemeier@fernuni-hagen.de