<abstract xmlns="http://www.w3.org/1999/xhtml">

<p>Conway’s introduction to algebraic operations on surreal numbers with a rather simple definition. However, he combines recursion with Conway’s induction on surreal numbers, more formally he combines transfinite induction-recursion with the properties of proper classes, which is diffcult to introduce formally.</p>
<p>This article represents a further step in our ongoing e orts to investigate the possibilities offered by Mizar with Tarski-Grothendieck set theory [<xref ref-type="bibr" rid="j_forma-2023-0020_ref_004">4</xref>] to introduce the algebraic structure of Conway numbers and to prove their ring character.</p>
</abstract>

Conway’s introduction to algebraic operations on surreal numbers with a rather simple definition. However, he combines recursion with Conway’s induction on surreal numbers, more formally he combines transfinite induction-recursion with the properties of proper classes, which is diffcult to introduce formally.
This article represents a further step in our ongoing e orts to investigate the possibilities offered by Mizar with Tarski-Grothendieck set theory [4] to introduce the algebraic structure of Conway numbers and to prove their ring character.

The Ring of Conway Numbers in Mizar

Formalized Mathematics

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

{"article-title":"The Ring of Conway Numbers in Mizar"}

Conway’s introduction to algebraic operations on surreal numbers with a rather simple definition. However, he combines recursion with Conway’s induction on...

The Ring of Conway Numbers in Mizar

Published Online: Dec 31, 2023

Page range: 215 - 228

Accepted: Dec 12, 2023

DOI: https://doi.org/10.2478/forma-2023-0020

Keywords
surreal numbers, Conway’s game

© 2023 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

The Ring of Conway Numbers in Mizar

Published Online: Dec 31, 2023

Page range: 215 - 228

Accepted: Dec 12, 2023

DOI: https://doi.org/10.2478/forma-2023-0020

Keywordssurreal numbers, Conway’s game

© 2023 Karol Pąk, published by Sciendo

This work is licensed under the Creative Commons Attribution-ShareAlike 3.0 Public License.

Keywords
surreal numbers, Conway’s game