@ARTICLE{SURREAL0.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Conway Numbers -- Formal Introduction},
  SECTION1 = {Construction of Games on $\alpha$-day},
  SECTION2 = {Construction of Preorder on the $\alpha$-day},
  SECTION3 = {The Preorder on the $\alpha$-day},
  SECTION4 = {Surreal Number as a Special Type of Abstract Game},
  SECTION5 = {The Preorder of Surreal Numbers},
  DAY = {12},
  MONTH = {December},
  YEAR = {2023},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {Surreal numbers \cite{Conway:2001}, a fascinating mathematical concept introduced by John Conway, 
  have attracted considerable interest due to their unique properties. 
  In this article, we formalize the basic concept of surreal numbers close to the original Conway's 
  convention in the field of combinatorial game theory. 
  We introduce the numbers simultaneously with a pre-order, following the idea of the von Neumann hierarchy of set construction
  realized in Tarski-Grothendieck set theory.\par
  We define the notion of $\alpha$-day, for a given relation $\leq_R$ satisfying the condition
  $x \leq_R y iff L_x\!\ll_R\!\{y\}\wedge \{x\}\!\ll_R\!R_y$.
  Then we extract the crucial dependencies between $\alpha$-day and the relation $\leq_R$ to remove the parameter $R$ and finally   define the concept of surreal numbers in the Mizar system.
  in a way that mimics the inductive-recursive definitions.\par
  The formalization follows \cite{Conway:2001,Ehrlich,Ehrlich2012}
  and is an independent approach to that introduced by R.~Nittka~\cite{CGAMES_1.ABS}.}}

@article{Ehrlich,
  author    = {Philp Ehrlich},
  title     = {Number Systems with Simplicity Hierarchies: {A} Generalization of
               {C}onway's Theory of Surreal Numbers},
  journal   = {J. Symb. Log.},
  volume    = {66},
  number    = {3},
  pages     = {1231--1258},
  year      = {2001},
  url       = {https://doi.org/10.2307/2695104},
  doi       = {10.2307/2695104},
  timestamp = {Sun, 28 May 2017 13:21:52 +0200},
  biburl    = {https://dblp.org/rec/journals/jsyml/Ehrlich01.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@ARTICLE{Ehrlich2012,
  AUTHOR =       {Philip Ehrlich},
  TITLE =        {The absolute arithmetic continuum and the unification of all numbers great and small},
  JOURNAL =      {Bulletion Symbolic Logic},
  YEAR =         {2012},
  volume =       {18},
  number =       {1},
  pages =        {1--45},
  doi = {10.2178/bsl/1327328438}
}

