<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

Data publikacji: 31 gru 2023

Zakres stron: 215 - 228

Przyjęty: 12 gru 2023

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

Słowa kluczowe
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

Data publikacji: 31 gru 2023

Zakres stron: 215 - 228

Przyjęty: 12 gru 2023

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

Słowa kluczowesurreal 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.

Słowa kluczowe
surreal numbers, Conway’s game