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