Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Karol Pąk, Cezary Kaliszyk

TL;DR

This work formalizes Conway's surreal numbers in the Mizar system by integrating two foundational approaches—Conway's day-based construction and Ehrlich's tree-theoretic model—via a bridge that leverages global choice and transfinite induction. It replaces transfinite induction-recursion with transfinite induction, enabling a streamlined, set-theoretic treatment (Day${}_{Ord}$) that stays compatible with Mizar's foundations, and it proves that surreal numbers form an ordered field, including the square root. The authors develop a robust framework for combining proofs from both approaches, define a general scheme for constructing arithmetic operations, and demonstrate that foundational subsets such as the integers, dyadics, reals, ordinals, and powers of $\omega$ embed naturally within the surreal numbers. The Conway Normal Form (CNF) is formalized by marrying Conway's canonical representation with Ehrlich's generalization, facilitating further formal developments in surreal number theory and enabling transfer across proof systems. This work thus provides a comprehensive, machine-checked foundation for surreal numbers and their algebraic structure, with potential applications to broader proof-theoretic and foundational research.

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

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

TL;DR

This work formalizes Conway's surreal numbers in the Mizar system by integrating two foundational approaches—Conway's day-based construction and Ehrlich's tree-theoretic model—via a bridge that leverages global choice and transfinite induction. It replaces transfinite induction-recursion with transfinite induction, enabling a streamlined, set-theoretic treatment (Day) that stays compatible with Mizar's foundations, and it proves that surreal numbers form an ordered field, including the square root. The authors develop a robust framework for combining proofs from both approaches, define a general scheme for constructing arithmetic operations, and demonstrate that foundational subsets such as the integers, dyadics, reals, ordinals, and powers of embed naturally within the surreal numbers. The Conway Normal Form (CNF) is formalized by marrying Conway's canonical representation with Ehrlich's generalization, facilitating further formal developments in surreal number theory and enabling transfer across proof systems. This work thus provides a comprehensive, machine-checked foundation for surreal numbers and their algebraic structure, with potential applications to broader proof-theoretic and foundational research.

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 . 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.
Paper Structure (6 sections, 4 theorems, 13 equations, 1 figure)

This paper contains 6 sections, 4 theorems, 13 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Mizar
  3. Introduction to Surreal Numbers
  4. Formal Set-theoretic Construction of Surreal Numbers
  5. The Surreal Numbers as a Field
  6. Reals and Ordinals as Subsets of Surreal

Key Result

Lemma 3

Let $Ord$ be a relation, $\alpha$ be an ordinal and $x\in\hbox{Games}\,{\alpha}$ such that $x\not\in \hbox{Day}_{Ord}\,{\alpha}$. Then for all ordinals $\beta$, $x\not\in \hbox{Day}_{Ord}\,{\beta}$.

Figures (1)

  • Figure 1: The relations between the numbers created in the first four days. The bottom part of each node give a representative of the equivalence class w.r.t. the $\thickapprox$ relation. The edge labels + and - correspond to the tree-theoretic interpretation of surreal numbers.

Theorems & Definitions (11)

  • Definition 1: tree-theoretic comparison
  • Definition 2: $\hbox{Day}_{Ord}\,{\alpha}$
  • Lemma 3
  • Definition 4
  • Definition 5: $\hbox{Prod}^{\,C}_{\,}$ and $\hbox{Prod}^{\,O}_{\,}$
  • Definition 6: Almost ${\mathbbmsl{N}\!o}$-order
  • Definition 7
  • Theorem 8
  • Theorem 9
  • Theorem 10
  • ...and 1 more