# Conway's Games and Some of their Basic Properties

Formalized Mathematics (2011)

• Volume: 19, Issue: 2, page 73-81
• ISSN: 1426-2630

top

## Abstract

top
We formulate a few basic concepts of J. H. Conway's theory of games based on his book [6]. This is a first step towards formalizing Conway's theory of numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a proper class that satisfies the axioms of a real-closed field) that includes the reals and ordinals, thus providing a uniform, independent and simple approach to these two constructions that does not go via the rational numbers and hence does for example not need the notion of a quotient field.In this first article on Conway's games, we provide a definition of games, their birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as a tool), their negates and their signs, together with some elementary properties of these notions. If one is interested only in Conway's numbers, it would have been easier to define them directly, but going via the notion of a game is a more general approach in the sense that a number is a special instance of a game and that there is a rich theory of games that are not numbers.The main obstacle in formulating these topics in Mizar is that all definitions are highly recursive, which is not entirely simple to translate into the Mizar language. For example, according to Conway's definition, a game is an object consisting of left and right options which are themselves games, and this is by definition the only way to construct a game. This cannot directly be translated into Mizar, but a theorem is included in the article which proves that our definition is equivalent to Conway's.

## How to cite

top

Robin Nittka. "Conway's Games and Some of their Basic Properties." Formalized Mathematics 19.2 (2011): 73-81. <http://eudml.org/doc/267379>.

@article{RobinNittka2011,
abstract = {We formulate a few basic concepts of J. H. Conway's theory of games based on his book [6]. This is a first step towards formalizing Conway's theory of numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a proper class that satisfies the axioms of a real-closed field) that includes the reals and ordinals, thus providing a uniform, independent and simple approach to these two constructions that does not go via the rational numbers and hence does for example not need the notion of a quotient field.In this first article on Conway's games, we provide a definition of games, their birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as a tool), their negates and their signs, together with some elementary properties of these notions. If one is interested only in Conway's numbers, it would have been easier to define them directly, but going via the notion of a game is a more general approach in the sense that a number is a special instance of a game and that there is a rich theory of games that are not numbers.The main obstacle in formulating these topics in Mizar is that all definitions are highly recursive, which is not entirely simple to translate into the Mizar language. For example, according to Conway's definition, a game is an object consisting of left and right options which are themselves games, and this is by definition the only way to construct a game. This cannot directly be translated into Mizar, but a theorem is included in the article which proves that our definition is equivalent to Conway's.},
author = {Robin Nittka},
journal = {Formalized Mathematics},
keywords = {Conway; numbers and games; basic concepts; Mizar; proof assistant; mathematic formalization},
language = {eng},
number = {2},
pages = {73-81},
title = {Conway's Games and Some of their Basic Properties},
url = {http://eudml.org/doc/267379},
volume = {19},
year = {2011},
}

TY - JOUR
AU - Robin Nittka
TI - Conway's Games and Some of their Basic Properties
JO - Formalized Mathematics
PY - 2011
VL - 19
IS - 2
SP - 73
EP - 81
AB - We formulate a few basic concepts of J. H. Conway's theory of games based on his book [6]. This is a first step towards formalizing Conway's theory of numbers into Mizar, which is an approach to proving the existence of a FIELD (i.e., a proper class that satisfies the axioms of a real-closed field) that includes the reals and ordinals, thus providing a uniform, independent and simple approach to these two constructions that does not go via the rational numbers and hence does for example not need the notion of a quotient field.In this first article on Conway's games, we provide a definition of games, their birthdays (or ranks), their trees (a notion which is not in Conway's book, but is useful as a tool), their negates and their signs, together with some elementary properties of these notions. If one is interested only in Conway's numbers, it would have been easier to define them directly, but going via the notion of a game is a more general approach in the sense that a number is a special instance of a game and that there is a rich theory of games that are not numbers.The main obstacle in formulating these topics in Mizar is that all definitions are highly recursive, which is not entirely simple to translate into the Mizar language. For example, according to Conway's definition, a game is an object consisting of left and right options which are themselves games, and this is by definition the only way to construct a game. This cannot directly be translated into Mizar, but a theorem is included in the article which proves that our definition is equivalent to Conway's.
LA - eng
KW - Conway; numbers and games; basic concepts; Mizar; proof assistant; mathematic formalization
UR - http://eudml.org/doc/267379
ER -

## References

top
1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
5. [5] Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
6. [6] J. H. Conway. On numbers and games. A K Peters Ltd., Natick, MA, second edition, 2001.
7. [7] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
8. [8] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
9. [9] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.

## NotesEmbed?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.