Document Open Access Logo

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

Authors Karol Pąk , Cezary Kaliszyk

PDF

File

Thumbnail PDF
PDF
LIPIcs.ITP.2024.29.pdf
  • Filesize: 0.94 MB
  • 18 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
Keywords
  • Surreal numbers
  • Conway normal form
  • Mizar

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

Cite As Get BibTex

Karol Pąk and Cezary Kaliszyk. Conway Normal Form: Bridging Approaches for Comprehensive Formalization of Surreal Numbers. In 15th International Conference on Interactive Theorem Proving (ITP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 309, pp. 29:1-29:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ITP.2024.29

Author Details

Karol Pąk
  • University of Białystok, Poland
Cezary Kaliszyk
  • University of Melbourne, Australia
  • University of Innsbruck, Austria

Funding

Supported by ERC PoC grant no. 101156734 FormalWeb3 and Cost action CA20111 EPN.

Supplementary Materials

References

  1. Maan T. Alabdullah, Essam El-Seidy, and Neveen S. Morcos. On numbers and games. International Journal of Scientific & Engineering Research, 11, February 2022. Google Scholar
  2. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pąk. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 2017. URL: https://doi.org/10.1007/s10817-017-9440-6.
  3. Grzegorz Bancerek, Czesław Byliński, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pąk, and Josef Urban. Mizar: State-of-the-art and Beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics - International Conference, CICM 2015, volume 9150 of LNCS, pages 261-279. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-20615-8_17.
  4. Chad E. Brown and Karol Pąk. A tale of two set theories. In Cezary Kaliszyk, Edwin C. Brady, Andrea Kohlhase, and Claudio Sacerdoti Coen, editors, Intelligent Computer Mathematics - 12th International Conference, CICM 2019, volume 11617 of LNCS, pages 44-60. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-23250-4_4.
  5. John H. Conway. On Numbers And Games. A K Peters Ltd., 2nd edition, 2001. First Edition: 1976. Google Scholar
  6. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log., 65(2):525-549, 2000. URL: https://doi.org/10.2307/2586554.
  7. Philip Ehrlich. The absolute arithmetic continuum and the unification of all numbers great and small. Bulletion Symbolic Logic, 18(1):1-45, 2012. URL: https://doi.org/10.2178/bsl/1327328438.
  8. Philp Ehrlich. Number systems with simplicity hierarchies: A generalization of Conway’s theory of surreal numbers. J. Symb. Log., 66(3):1231-1258, 2001. URL: https://doi.org/10.2307/2695104.
  9. Adam Grabowski and Artur Korniłowicz. Implementing more explicit definitional expansions in mizar (short paper). In Adam Naumowicz and René Thiemann, editors, 14th International Conference on Interactive Theorem Proving, ITP 2023, July 31 to August 4, 2023, Białystok, Poland, volume 268 of LIPIcs, pages 37:1-37:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. URL: https://doi.org/10.4230/LIPICS.ITP.2023.37.
  10. Adam Grabowski, Artur Korniłowicz, and Adam Naumowicz. Four decades of Mizar. Journal of Automated Reasoning, 55(3):191-198, 2015. URL: https://doi.org/10.1007/s10817-015-9345-1.
  11. Gretchen Grimm. An introduction to surreal numbers, 2012. Google Scholar
  12. Cezary Kaliszyk and Karol Pąk. Semantics of Mizar as an Isabelle object logic. Journal of Automated Reasoning, 63(3):557-595, 2019. URL: https://doi.org/10.1007/S10817-018-9479-Z.
  13. Sebastian Koch. Natural addition of ordinals. Formalized Mathematics, 27(2):139-152, 2019. URL: https://doi.org/10.2478/forma-2019-0015.
  14. Lionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filliâtre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, TYPES 2004, volume 3839 of LNCS, pages 170-185. Springer, 2004. URL: https://doi.org/10.1007/11617990_11.
  15. Norman D. Megill. Metamath: A Computer Language for Pure Mathematics. Lulu Press, Morrisville, North Carolina, 2007. Google Scholar
  16. Robin Nittka. Conway’s games and some of their basic properties. Formalized Mathematics, 9(2):73-71, 2011. Google Scholar
  17. Steven Obua. Partizan games in Isabelle/HOLZF. In Kamel Barkaoui, Ana Cavalcanti, and Antonio Cerone, editors, Theoretical Aspects of Computing - ICTAC 2006, volume 4281 of LNCS, pages 272-286. Springer, 2006. Google Scholar
  18. Lawrence C. Paulson. Set theory for verification: I. From foundations to functions. J. Autom. Reasoning, 11(3):353-389, 1993. URL: https://doi.org/10.1007/BF00881873.
  19. Karol Pąk. Conway numbers - formal introduction. Formalized Mathematics, 31(1):193-203, 2023. URL: https://doi.org/10.2478/forma-2023-0018.
  20. Karol Pąk. Integration of game theoretic and tree theoretic approaches to Conway numbers. Formalized Mathematics, 31(1):205-213, 2023. URL: https://doi.org/10.2478/forma-2023-0019.
  21. Karol Pąk. The ring of Conway numbers in Mizar. Formalized Mathematics, 31(1):215-228, 2023. URL: https://doi.org/10.2478/forma-2023-0020.
  22. Dierk Schleicher and Michael Stoll. An introduction to Conway’s games and numbers. Moscow Mathematical Journal, 6, 2004. URL: https://doi.org/10.17323/1609-4514-2006-6-2-359-388.
  23. Claus Tøndering. Surreal numbers-an introduction. HTTP, version 1.7, December 2019. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact