REPOZYTORIUM UNIWERSYTETU
W BIAŁYMSTOKU
UwB

  1. Repozytorium Uniwersytetu w Białymstoku
  2. Czasopisma naukowe / Journals
  3. Formalized Mathematics
  4. Formalized Mathematics, 2025, Volume 33, Issue 1

Szukanie zaawansowane
  • Zespoły i Kolekcje


  • Zaloguj się
  • Zarejestruj się
  • Mój RUB
  • FAQ
  • Polityka
  • Regulamin
  • DOI
  • Instrukcja
  • Aspekty prawne
  • Open Access
  • Archiwum


  • Kontakt
  • O Dspace
  • Strona Biblioteki
  • Strona Uczelni



    • Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji: http://hdl.handle.net/11320/19593
    Pełny rekord metadanych
    Pole DCWartośćJęzyk
    dc.contributor.authorPąk, Karol-
    dc.date.accessioned2026-01-09T11:17:18Z-
    dc.date.available2026-01-09T11:17:18Z-
    dc.date.issued2025-
    dc.identifier.citationFormalized Mathematics, Volume 33, Issue 1, Pages 11-23pl
    dc.identifier.issn1426-2630-
    dc.identifier.urihttp://hdl.handle.net/11320/19593-
    dc.description.abstractThe concept of surreal numbers, as postulated by John Conway, represents a complex and multifaceted structure that encompasses a multitude of familiar number systems, including the real numbers, as integral components. In this study, we undertake the construction of the real numbers, commencing with the integers and dyadic rationals as preliminary steps. We proceed to contrast the resulting set of real numbers derived from our construction with the axiomatically defined set of real numbers based on Conway’s axiom. Our findings reveal that both approaches culminate in the same set.pl
    dc.language.isoenpl
    dc.publisherUniversity of Białystokpl
    dc.rightsAttribution-ShareAlike 4.0 International (CC BY-SA 4.0)pl
    dc.rights.urihttps://creativecommons.org/licenses/by-sa/4.0/pl
    dc.subjectsurreal numberpl
    dc.subjectConway’s gamepl
    dc.subjectdyadic numberpl
    dc.titleSurreal Dyadic and Real Numbers: A Formal Constructionpl
    dc.typeArticlepl
    dc.rights.holder© 2025 The Author(s)pl
    dc.rights.holderCC BY-SA 4.0 licensepl
    dc.identifier.doi10.2478/forma-2025-0002-
    dc.description.AffiliationFaculty of Computer Science, University of Białystok, Polandpl
    dc.description.referencesVincent Bagayoko and Joris van der Hoeven. Surreal substructures. Fundamenta Mathematicae, 266(1):25–96, 2024. doi:10.4064/fm231020-23-2.pl
    dc.description.referencesWolfgang Bertram. On Conway’s numbers and games, the von Neumann universe, and pure set theory. ArXiv preprint arXiv:2501.04412, 2025.pl
    dc.description.referencesJohn Horton Conway. On Numbers and Games. A K Peters Ltd., Natick, MA, second edition, 2001. ISBN 1-56881-127-6.pl
    dc.description.referencesOvidiu Costin and Philip Ehrlich. Integration on the surreals. Advances in Mathematics, 452:109823, 2024. doi:10.1016/j.aim.2024.109823.pl
    dc.description.referencesPeter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525–549, 2000. doi:10.2307/2586554.pl
    dc.description.referencesPhilip Ehrlich. The absolute arithmetic continuum and the unification of all numbers great and small. The Bulletin of Symbolic Logic, 18(1):1–45, 2012. doi:10.2178/bsl/1327328438.pl
    dc.description.referencesPhilp Ehrlich. Number systems with simplicity hierarchies: A generalization of Conway’s theory of surreal numbers. Journal of Symbolic Logic, 66(3):1231–1258, 2001. doi:10.2307/2695104.pl
    dc.description.referencesHarry Gonshor. An Introduction to the Theory of Surreal Numbers. London Mathematical Society Lecture Note Series, 110. Cambridge University Press, 1986. ISBN 0521312051.pl
    dc.description.referencesDonald E. Knuth. Surreal Numbers: How Two Ex-students Turned on to Pure Mathema tics and Found Total Happiness. Addison-Wesley, 1974.pl
    dc.description.referencesLionel Elie Mamane. Surreal numbers in Coq. In Jean-Christophe Filliˆatre, Christine Paulin-Mohring, and Benjamin Werner, editors, Types for Proofs and Programs, TYPES 2004, volume 3839 of LNCS, pages 170–185. Springer, 2004. doi:10.1007/11617990_11.pl
    dc.description.referencesJ. A. Nieto, J. A. Escalante-Javalera, C. A. Somera-Patrón, and E. J. Villasenor-Gonz´alez. Parity of dyadic rationals and surreal numbers. Far East Journal of Mathematical Sciences (FJMS), (2):155–167, May 2024. doi:10.17654/0972087124010.pl
    dc.description.referencesSteven 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.pl
    dc.description.referencesKarol Pąk. Conway numbers – formal introduction. Formalized Mathematics, 31(1): 193–203, 2023. doi:10.2478/forma-2023-0018.pl
    dc.description.referencesKarol Pąk. Integration of game theoretic and tree theoretic approaches to Conway numbers. Formalized Mathematics, 31(1):205–213, 2023. doi:10.2478/forma-2023-0019.pl
    dc.description.referencesKarol Pąk. The ring of Conway numbers in Mizar. Formalized Mathematics, 31(1): 215–228, 2023. doi:10.2478/forma-2023-0020.pl
    dc.description.referencesKarol Pąk and Cezary Kaliszyk. Conway normal form: Bridging approaches for comprehensive formalization of surreal numbers. In Yves Bertot, Temur Kutsia, and Michael Nor rish, editors, 15th International Conference on Interactive Theorem Proving, ITP 2024, September 9-14, 2024, Tbilisi, Georgia, volume 309 of LIPIcs, pages 29:1–29:18. Schloss Dagstuhl – Leibniz-Zentrum f¨ur Informatik, 2024. doi:10.4230/LIPICS.ITP.2024.29.pl
    dc.description.referencesMatthew Roughan. Practically surreal: surreal arithmetic in Julia. SoftwareX, 9:293–298, 2019. doi:10.1016/j.softx.2019.03.005.pl
    dc.description.referencesAlex Ryba, Philip Ehrlich, Richard Kenyon, Jeffrey Lagarias, James Propp, and Louis Kauffman. Conway’s mathematics after Conway. Notices of the American Mathematical Society, 69:1145–1155, 2022. doi:10.1090/noti2513.pl
    dc.description.referencesDominik Tomaszuk, Łukasz Szeremeta, and Artur Korniłowicz. MMLKG: Knowledge graph for mathematical definitions, statements and proofs. Scientific Data, 10(1), 2023. doi:10.1038/s41597-023-02681-3.pl
    dc.description.referencesClaus Tøndering. Surreal numbers – an introduction. HTTP, version 1.7, December 2019.pl
    dc.description.referencesThe Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.pl
    dc.description.referencesMakarius Wenzel, Lawrence C. Paulson, and Tobias Nipkow. The Isabelle framework. In Otmane Ait Mohamed, C´esar Mu˜noz, and Sofi`ene Tahar, editors, Theorem Proving in Higher Order Logics, pages 33–38. Springer Berlin Heidelberg, 2008.pl
    dc.identifier.eissn1898-9934-
    dc.description.volume33pl
    dc.description.issue1pl
    dc.description.firstpage11pl
    dc.description.lastpage23pl
    dc.identifier.citation2Formalized Mathematicspl
    dc.identifier.orcid0000-0002-7099-1669-
    Występuje w kolekcji(ach):Formalized Mathematics, 2025, Volume 33, Issue 1

    Pliki w tej pozycji:
    Plik Opis RozmiarFormat 
    Surreal_Dyadic_and_Real_Numbers_A_Formal_Construction.pdf333,09 kBAdobe PDFOtwórz
    Pokaż uproszczony widok rekordu Zobacz statystyki


    Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons