<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

Publicado en línea: 31 dic 2023

Páginas: 215 - 228

Aceptado: 12 dic 2023

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

Palabras clave
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

Publicado en línea: 31 dic 2023

Páginas: 215 - 228

Aceptado: 12 dic 2023

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

Palabras clavesurreal 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.

Palabras clave
surreal numbers, Conway’s game