Since ordered fields can always be split into two halves whose only common element is $0$, namely $(\leftarrow,0]$ and $[0,\rightarrow),$ I was wondering if we can axiomatize just the right half. Note that the left half fails to be closed under products, so its not a good candidate for axiomatization.
Anyway, has anyone done this?
If not, here's a not overly-serious proposal. Start with the ordered field axioms, drop the requirement that every number have an additive inverse, and add weaker the requirement that if $x \leq y$, then there exists $k$ such that $x+k=y$. This new system of axioms is still satisfied by every ordered field, so in order to exclude them, we also assume that $0 \leq x$ for all $x$. We can also drop the axiom that if $x \geq 0$ and $y \geq 0$, then $xy \geq 0$, since this is immediate.
I don't know if this really works - we want a natural bijection between the class of all ordered fields and the class of all 'right halves.'
A bit of motivation.
Firstly, I like the idea that there are many ways to obtain $\mathbb{R}$. The 'usual' approach is to begin with $\mathbb{N}$, adjoin negatives to obtain $\mathbb{Z}$, adjoin products and reciprocals to obtain $\mathbb{Q}$, and finally adjoin suprema to obtain $\mathbb{R}.$
Another approach would be to begin with $\mathbb{N}$, adjoin reciprocals and products to obtain$[0,\rightarrow)_\mathbb{Q}$, adjoin suprema to obtain $[0,\rightarrow)_\mathbb{R}$, and finally adjoin negatives to obtain $\mathbb{R}.$
Now the step where suprema are adjoined is basically just completion via Dedekind cuts. But, in the usual approach, where negative numbers are adjoined right at the outset, products of Dedekind cuts are messy to define. This problem does not arise, though, in the latter approach.
A similar issue seems to appear in Conway's 'On Numbers And Games,' where the product of Surreal numbers is rather messy (I only just received this book, hence the question). So I'm wondering if Conway's definition of the product of Surreal numbers can be simplified by restricting ourselves to the non-negative numbers, and only adjoining additive inverses afterwards.
I believe the answer is yes.
This is because for any positive part of the ordered field, we can define an extension of a structure $(X,\leq,+,\cdot,0,1)$ to an ordered field in the usual manner, by identifying the ordered pair $(x,0)$ with $x$ and $(x,1)$ with $-x$.
It shouldn't be hard to check that this extension satisfies the axioms of field whenever the $X$ satisfies the theory of the positive part of an ordered field.