Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers

TL;DR

This paper formalizes Conway's surreal numbers in Mizar using two approaches, creating a bridge between them to enhance formalization, and proves key properties like the field structure and Normal Form.

Contribution

It introduces a unified formalization method for surreal numbers, combining two approaches and proving their fundamental properties within a proof assistant.

Findings

Surreal numbers form a field including reals, ordinals, and infinitesimals.

The paper demonstrates the Normal Form of surreal numbers.

A bridge between two formalization approaches is established.

Abstract

The proper class of Conway's surreal numbers forms a rich totally ordered algebraically closed field with many arithmetic and algebraic properties close to those of real numbers, the ordinals, and infinitesimal numbers. In this paper, we formalize the construction of Conway's numbers in Mizar using two approaches and propose a bridge between them, aiming to combine their advantages for efficient formalization. By replacing transfinite induction-recursion with transfinite induction, we streamline their construction. Additionally, we introduce a method to merge proofs from both approaches using global choice, facilitating formal proof. We demonstrate that surreal numbers form a field, including the square root, and that they encompass subsets such as reals, ordinals, and powers of $\omega$. We combined Conway's work with Ehrlich's generalization to formally prove Conway's Normal Form, paving the way for many formal developments in surreal number theory.