Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers
Fuente:
arXiv
Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866913524777746432 |
|---|---|
| author | Pąk, Karol Kaliszyk, Cezary |
| author_facet | Pąk, Karol Kaliszyk, Cezary |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2410_00065 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers Pąk, Karol Kaliszyk, Cezary Logic in Computer Science 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. |
| title | Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2410.00065 |