<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

Online veröffentlicht: 31. Dez. 2023

Seitenbereich: 215 - 228

Akzeptiert: 12. Dez. 2023

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

Schlüsselwörter
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

Online veröffentlicht: 31. Dez. 2023

Seitenbereich: 215 - 228

Akzeptiert: 12. Dez. 2023

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

Schlüsselwörtersurreal 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.

Schlüsselwörter
surreal numbers, Conway’s game