I'm trying not to be offended, I know how spam filters work and sometimes someone gets wrongly accused and it just happens to be me. I'm just a little frustrated because I carefully craft this question for over an hour, then I get "this looks like spam" with absolutely no suggestion to make it look less like it.
My Notepad++ counts 913 "\w+" instances (so around 913 words), I use 2 links, 2 strongly marked phases ("Theorem 10." and "Here is my problem:"), 3 cursive parts (also short) and 5 lines beginning with > (quotes). Removing links and formatting hasn't helped. I could just shorten the question by leaving parts out and just edit them in again, but that seems cheap and is possibly unwanted.
Please tell me what I can do?
Edit: Original Post at https://pastebin.com/jvt9jPuD and below (first line was heading)
Is the inverse of surreal numbers actually well-defined?
J.Conway wrote in his book "On numbers and games" (1st edition, 1976) on p. 66
It seems to us, however, that mathematics has now reached the stage where formalization within some particular axiomatic set theory is irrelevant, even for foundational studies.
I happen to disagree. In fact, I'm having some fun formalizing mathematics in the Mizar system, which has just one article on Conway games yet. I want to find out if further formalization would be fruitful, i.e. if the operations defined in the book can be formalized at all. The cited article only defines $-x$ for a game $x$, but gives a pretty good idea how to deal with the highly inductive nature of games and I'm certain I could formalize addition and multiplication. What bothers me is the definition of $y=\frac{1}{x}$, given by $$y=\left\{\left.0,\frac{1+(x^R-x)y^L}{x^R},\frac{1+(x^L-x)y^R}{x^L}\right|\frac{1+(x^L-x)y^L}{x^L},\frac{1+(x^R-x)y^R}{x^R}\right\}$$ for $x$ positive and only positive $x^L$ considered, which is needed for defining division. Conway, after giving this definition on p.21, writes himself
Note that expressions involving $y^L$ and $y^R$ appear in the definition of $y$. It is this that requires us to "explain" the definition. The explanation is that we regard these parts of the definition as defining new options for $y$ in terms of old ones.
In a footnote, the rather trivial example of $\frac{1}{3}=\{0,\frac{1}{4},\frac{5}{16},\ldots|\frac{1}{2},\frac{3}{8},\ldots\}$ is given to show "how the definition works".
I can't see why $y$ is well defined in general. For example, given two uncountable cardinals $\alpha<\beta$ I'm having a hard time seeing how $\frac{1}{\beta-\alpha}$ should be computed. The emphasis here lies on "uncountable".
Claus Tøndering gave a seemingly equivalent definition of the inverse here on p.44 (if the definition should not be equivalent, please point out why). He defines $y$ through $y^L$ and $y^R$ as such: $$0\in y^L$$ $$z\in y^L \Rightarrow \tfrac{1+(x^R-x)z}{x^R}\in y^L, \tfrac{1+(x^L-x)z}{x^L}\in y^R$$ $$z\in y^R \Rightarrow \tfrac{1+(x^L-x)z}{x^L}\in y^L, \tfrac{1+(x^R-x)z}{x^R}\in y^R$$
This is still "too" recursive to be formalized. One of my problems is that I can't comprehend the cardinality of $y^L$ and $y^R$. I mean, I could define $y^L_0 = \{0\}, y^R_0 = \{\}$ and for $n\in\mathbb{N}, n>0$ change Tønderings definitions to $z\in y^L_{n-1} \Rightarrow \ldots\in y^L_n$ and so on (or better: $$y^L_n = \left\{\left.\tfrac{1+(x^R-x)z}{x^R}\right|z\in y^L_{n-1}\right\}\cup\left\{\left.\tfrac{1+(x^L-x)z}{x^L}\in y^L \right|z\in y^R_{n-1}\right\}$$ and $y^R$ analogue) and conjecture $$y^L = \{0\}\cup\bigcup_{n\in\mathbb{N}} y^L_n,\quad y^R = \bigcup_{n\in\mathbb{N}} y^R_n$$
Here is my problem: I really doubt I could prove that. First off, I'm having trouble believing the equality holds, that I could miss something by merely having a countable union. Secondly, $y^L$ and $y^R$ are required to be sets and I can image how they accidentally could become classes this way with some $x$ nefarious enough (maybe $x=\beta-\alpha$ is enough already?), because maybe the set generation process never stops at a certain day. I get couldn't information about this topic at all. In papers about surreal numbers either they are just given like here without further doubt or not explicitly given at all. Some papers, like these from Philip Ehrlich, go deeper into cardinality or other theories above my understanding, so if the issue would be resolved there, I wouldn't have noticed.
On the matter of the $y^L_n$ and $y^R_n$ being sets, Conway writes
Theorem 10. We have (i) $xy^L<1<xy^R$ for all $y^L,y^R$.
(ii) $y$ is a number. [(iii) and (iv) left out]
Proof. We observe that the options of $y$ are defined by formulae of the form $$y''=\frac{1+(x'-x)y'}{x'}$$ where $y''$ is an earlier option of $y$, and $x'$ some non-zero-option of $x$. This formula can be written $$1-xy'' = (1-xy')\frac{x'-x}{x'}$$ which shows that $y''$ satisfies (i) if $y'$ does. Plainly $0$ does. Part (ii) now follows, since we cannot have any inequality $y^L\geq y^R$. [...]
As far as my understanding goes, with "$y$ is a number" he means "if $y$ is a game, then it's a number", as this proof (directly following the remark after the definition) does not indicate the sethood of $y^L$ or $y_R$ in my eyes.
