7
$\begingroup$

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: Could the left or right options of $y$ accidentally be a proper class? I really doubt I could prove that's wrong. 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.

Improve this question
$\endgroup$
7
  • 3
    $\begingroup$ Surreal numbers definitely cannot be represented in general by countable left and right sets. For example, there is no representation of $\omega_1$ with a countable left set, since every such set would be bounded below $\omega_1$, and so an earlier-born ordinal would fill the cut. Is that your question? $\endgroup$
    – Joel David Hamkins
    Commented Dec 7, 2017 at 14:42
  • $\begingroup$ @JoelDavidHamkins It is not. I'm aware of $\omega_1$. The core of the question is, when forming the inverse of $x>0$, could the left or right options of $\frac{1}{x}$ accidentically be a proper class? If not, why? $\endgroup$
    – SK19
    Commented Dec 8, 2017 at 20:46
  • $\begingroup$ @JoelDavidHamkins : In this instance the $y_L,y_R$ need not be simpler than $y$ so it is not impossible that $y_L,y_R$ be a countable representation of $y$, like $\omega_1 - 1,\varnothing$ is a countable representation of $\omega_1$. $\endgroup$
    – nombre
    Commented Dec 9, 2017 at 11:10
  • 2
    $\begingroup$ That kind of situation happens in many subjects, and I find it usually to be a good thing, since sometimes one wants one perspective and sometimes one wants the other. It is often helpful to play two perspectives off against one another. $\endgroup$
    – Joel David Hamkins
    Commented Dec 9, 2017 at 11:49
  • 1
    $\begingroup$ I don't understand what the issue is in this question. You've given an explicit unwinding of the genetic definition that manifestly exhibits each of the collections of options of $y$ as being sets: they are countable unions of sequences of sets that are defined recursively; each $y^L_{n+1}$ is a set because $y^L_n$ is a set (recursively) and $x^R$ is a set (by assumption). To formalize this in ZFC the axiom of replacement is probably needed, but that's not surprising. $\endgroup$
    – Mike Shulman
    Commented Jul 29, 2018 at 4:09

1 Answer 1

Reset to default
8
$\begingroup$

I think that you could take this as $y$ admitting the definition $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\}$ where as you defined them, $Y_L := \{0\} \cup \bigcup \limits_{n \in \mathbb{N}} y_n^L$ and $Y_R := \bigcup \limits_{n \in \mathbb{N}} y_n^R$. (note: I have not checked that this works so I might be wrong)

Then $Y_L \subsetneq y_L$ and $Y_R \subsetneq y_R$, but now tat $y$ is defined, we can see that it satisfies the equation $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\}$.

If you don't like this kind of approach, know that Gonshor does all the dirty work in a rigorous way in his monograph An Introduction to the Theory of Surreal Numbers.

Improve this answer
$\endgroup$
3
  • $\begingroup$ Your approach is fine, I think I just have to prove my way through showing everything works as it should. This will take some time. When I have results, I will report them here. Thanks for the Gonshor reference, his definition for the inverse at least seems to ensure sethood of the options of the inverse. But I will need some time to work this through. $\endgroup$
    – SK19
    Commented Dec 8, 2017 at 21:08
  • 1
    $\begingroup$ It may be that my explanation is false and that what Conway really intended was that one should define $y_{\omega}$ as I stated, and then if $y_{\omega}$ does not satisfy the equality, keep defining the $y_{\omega+n}^L$ and so on until it works. But this might work as you probably saw that Gonshor uses the same type of arguments which only requires countably many operations. Note that there is a "simple way" to prove the existence of inverses once the normal form is known, but the normal form requires the definition of inverses of real numbers. Good luck! $\endgroup$
    – nombre
    Commented Dec 8, 2017 at 21:26
  • 1
    $\begingroup$ I had the same doubt than the OP not so long ago. I've done all the dirty work required and I can confirm that works exactly like nombre has said. It is not required to use higher ordinais, an enumerable sequence of sets will do the job. $\endgroup$
    – Anderson Brasil
    Commented Sep 7, 2020 at 19:34

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .