The Ring of Conway Numbers in Mizar

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 difficult to introduce formally. This article represents a further step in our ongoing efforts 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.