@ARTICLE{SURREALI.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Inverse Element for Surreal Number},
  SECTION1 = {Construction of the Inverse Element for Surreal Numbers},
  SECTION2 = {The Concept of Positive Options in Conway's Sense},
  SECTION3 = {The Inverse Element for Surreal Numbers},
  SECTION4 = {Selected Properties of the Inverse Element},
  DAY = {22},
  MONTH = {October},
  YEAR = {2024},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {
Conway's surreal numbers have a fascinating algebraic structure,
which we try to formalise in the Mizar system. In this article,
building on our previous work establishing that the surreal numbers fulfil the ring properties,
we construct the inverse element for any non-zero number.
For that purpose, we formalise the definition of the inverse element formulated in Section {\it Properties of Division} of Conway's book.
In this way we show formally in the Mizar system that surreal numbers satisfy all nine properties of a field.},
INTRODUCTION = {In our previous work~\cite{SURREALR}, we have formally defined and justified a list of
properties of subtraction, addition and multiplication. The definition of division,
which has been missing so far, is, however, significantly more complicated than the other operations.
For a number $x=\{L_x\mid R_x\}$ to be a positive surreal number where $0 \in L_x$ and all other members of $L_x$ are positive,
Conway~\cite{conway} define $y$ as follows:
\begin{equation}\label{SURREALIeq1}
y=\left\{0,\frac{1+(x^R\!-\!x)y^L}{x^R}, \frac{1+(x^L\!-\!x)y^R}{x^L}\mid
\frac{1+(x^L\!-\!x)y^L}{x^L}, \frac{1+(x^R\!-\!x)y^R}{x^R}    \right\}
\end{equation}
where $x^L$, $x^R$ ranges over all positive members of set $L_x$, $R_x$, respectively~\cite{Conway:2001}.
The definition, like most of Conway's, is rather confusing and seems to
be based more on the property of the inverse element than on a typical mathematical definition.
In fact, $y=\{L_y\mid R_y\}$ is defined by a kind of hidden recursion
since $y^L$, $y^R$ which appear on the RHS of the equation~\eqref{SURREALIeq1}
are members of $L_y$, $R_y$. As an illustration of this definition, Conway gave the example $3=\{0,2\mid\;\}$,
where there is only $x^L=2$, $y=\{0,\ldots\mid \ldots\}$ is given as an initial value,
so we can put $y^L=0$. Then  $\frac{1+(2-3)0}{2}=\frac{1}{2}$ is a new $y^R$,
and $\frac{1+(2-3)\frac{1}{2}}{2} = \frac{1}{4}$ is a new $y^L$ and so on, an infinite number of times.
Finally
$y = \{0,\frac{1}{4}, \frac{5}{16},\frac{21}{64},  \frac{85}{256}, \ldots
\mid \frac{1}{2}, \frac{3}{8}, \frac{11}{32}, \frac{43}{128},\ldots\}$.
\par
This definition with a double recursion is a challenge to the formal approach.
Mamane, in his formalisation in the Coq system~\cite{Mamane04},
considered the construction of the inverse element as a future work.
Obua formalised the surreal numbers in the Isabelle/HOLZF by covering only the additive group~\cite{Obua06}.
Schleicher and Stoll~\cite{schleicher} proposed a reasonably precise informal proof
that we adapt in our approach.
\par
To formalise such a concept, we first introduce a restriction that limits the members of the sets
$L_x$, $R_x$ to those that are positive
with special exception in $L_x$, where we added $0$.
Let $x$ be a positive surreal number. We define $\| x \|$ (see \ref{Def9}) to be
\begin{equation}
\{0, \{x^L \in L_x \mid x^L >0\}\mid \{x^R \in R_x \mid x^R >0\}\}
\end{equation}
and we prove that $x\approx \| x \|$ (see \ref{Th18}).
\newcommand{\DIV}[0]{\texttt{d}}
Then we focus on the fact that the definition of the inverse element $x^{-1}$ has looping,
i.e. the definition uses the values of the inverse element of every positive member of
the sets $L_x$, $R_x$, but they have to be born before $x$.
Suppose $I$ is a function, which in context, will be the corresponding inverse function defined
on all the positive surreal numbers that were born before $x$, in particular on $L_x\cup R_x$.
 We define a subset of surreal numbers
  as follows (see \ref{Def2},\ref{Def3}):
\begin{definitionKP}[Def2,Def3]
 Let $x$ be a surreal number, $X,P$ be surreal number sets, and $I$
 be a function from the surreal numbers to the surreal numbers such that
  $X$ is a subset of the domain of $I$. We define a subset of surreal numbers
  as follows:
\begin{equation}
    \DIV(P,x,X,I)=\bigcup_{p\in P}\{ (1+(a-x)\cdot p)\cdot I(a)\mid a\in X\}.
\end{equation}
\end{definitionKP}
\noindent
We define also a sequence of sets of surreal numbers $\DIV^L_n(x,I)$, $\DIV^R_n(x,I)$
for a given surreal number $x$ and a function $I$ recursively as follows:
 \begin{equation}
  \begin{aligned}
  \DIV_0^L(x,I) &= \{0\},\\ \DIV_0^R(x,I) &= \emptyset,\\
  \DIV_{n\!+\!1}^L(x,I)& = \DIV_{n}^L(x,I) \cup
   \DIV(\DIV_{n}^L(x,I),x,R_x,I) \cup \DIV(\DIV_{n}^R(x,I),x,L_x,I),\\
   \DIV_{n\!+\!1}^R(x,I)& = \DIV_{n\!+\!1}^R(x,I) \cup
        \DIV(\DIV_{n}^L(x,I),x,L_x,I)\cup \DIV(\DIV_{n}^R(x,I),x,R_x,I).
\end{aligned}
\end{equation}
We show that $\bigcup_{n\in\mathbb{N}} \DIV_n^L(x,I)$,
$\bigcup_{n\in\mathbb{N}} \DIV_n^R(x,I)$ are sets of surreal numbers
if $I$ is a surreal-valued function on $L_x\cup R_x$.
Next we restrict our consideration to the positive surreal number $x$, where we have
$x \approx \| x \|$. Note that $\texttt{born}\,\| x \|\leq \texttt{born}\,x$ (see \ref{22}). Without loss of generality we can
assume $\texttt{born}\,\| x \|= \texttt{born}\,x$.
Then exploring the assumption that $I(a)\cdot a \approx 1$ for
all the positive surreal numbers $a$ that were born before $a$,
we can prove the following key step that
\begin{equation}
y=\{\bigcup_{n\in\mathbb{N}} \DIV_n^L(\|x\|,I)\mid
\bigcup_{n\in\mathbb{N}} \DIV_n^R(\|x\|,I)\}
\end{equation}
is a surreal number (see \ref{Th31}) and $x\cdot y \approx 1$ (see \ref{Th32}).
\par
It is easy to see that, based on this step, we can extend the domain of the function $I$, which covers all surreal numbers created in days before $\alpha$, by all positive surreal numbers born on day $\alpha$, where $\alpha$ is an ordinal number.
Consequently, using second-order schemes formulated in \cite{SURREALR} which are a consequence of transfinite induction, we construct a unique sequence of $\{I_\alpha\}$ functions, where $I_\alpha$ is the inverse function defined on day $\alpha$. Finally, we define $x^{-1}$ as $I_\alpha(x)$ (see \ref{Def13,Def14}), where $\alpha$ is a day where a given positive $x$ is born and
$-I_\alpha(-x)$ in the negative case.
\par
Our formal construction of the inverse element seems to differ from the definition proposed \eqref{SURREALIeq1} by Conway.
This difficulty can be avoided by directly using transfinite induction-recursion, which is not available in the Mizar system.
We test our approach by proving that our concept of an inverse element satisfies the property formulated by Conway.
\begin{theoremKP}{\ref{Th31},\ref{Th32}}\\
Let $x$ be a positive surreal number. We define
$\DIV(A,x,B) = \{(1 +(a\!-\!x)\cdot b)\cdot  (a^{-1}) | a \in A \wedge  b \in B \wedge 0 < a\}$.
Then
\begin{equation}
x^{-1} \approx \{ \{0\}\cup \DIV(R_x,x,L_{x^{-1} })\cup \DIV(L_x,x,R_{x^{-1}}),
\DIV(L_x,x,L_{x^{-1}})\cup \DIV(R_x,x,R_{x^{-1}})\}.
\end{equation}
\end{theoremKP}}
}

@inproceedings{Mamane04,
  author    = {Lionel Elie Mamane},
  editor    = {Jean{-}Christophe Filli{\^{a}}tre and
               Christine Paulin{-}Mohring and
               Benjamin Werner},
  title     = {Surreal Numbers in {C}oq},
  booktitle = {Types for Proofs and Programs, {TYPES} 2004},
  series    = {LNCS},
  volume    = {3839},
  pages     = {170--185},
  publisher = {Springer},
  year      = {2004},
  url       = {https://doi.org/10.1007/11617990\_11},
  doi       = {10.1007/11617990\_11},
  timestamp = {Tue, 14 May 2019 10:00:42 +0200},
  biburl    = {https://dblp.org/rec/conf/types/Mamane04.bib},
  bibsource = {dblp computer science bibliography, https://dblp.org}
}

@inproceedings{Obua06,
  author    = {Steven Obua},
  title     = {Partizan Games in {Isabelle/HOLZF}},
  booktitle = {Theoretical Aspects of Computing -- {ICTAC} 2006},
  pages     = {272--286},
  year      = {2006},
  editor    = {Kamel Barkaoui and
               Ana Cavalcanti and
               Antonio Cerone},
  series    = {LNCS},
  volume    = {4281},
  publisher = {Springer},
}