Constructing the real numbers from the nonnegative real numbers I have read Ittay Weiss' survey on constructions of the real numbers: https://arxiv.org/abs/1506.03467
He writes that it is basically sufficient to construct the positive real numbers, as inverses (and 0) can be added in a final step. I was wondering how this works exactly. I am aware of the Grothendieck group construction: we can embed a semigroup in an abelian group by considering pairs of elements of the semigroup (representing their difference). 
Is this sufficient? That is, can we simply apply this procedure to a totally ordered semifield (namely $\mathbb R_{\ge0}$) and expect to automatically get a totally ordered field? I have been unable to find a reference for this statement, and I am not sure how I would show this.
 A: The common approach is to define an operation on $\def\R{\Bbb R^+} \def\x{\times} K=(\R,+)\x(\R,+)$ and then establish an equivalence relation to factor out the "superfluous" pairs resp. the ambiguity of representation.  This will be an analogue route to how $\Bbb Q$ can be constructed from $\Bbb Z$, or $\Bbb Z$ can be constructed from $\Bbb N$ just to name a few.
Every Real number can be represented in a non-unique way as difference of two positive Real numbers, so the operation will represent a difference without using operations / notations like $-x$ or $x-y$ which we don't have yet.  The non-uniqueness will be addressed by considering equivalence classes, and these classes will later on be called "Real numbers".
Specifically, define a binary operation + as
\begin{align}
+:K\x K&\to K \\
(x,y) + (x',y') &\mapsto (x+x',y+y')
\end{align}
The pairs should function as a difference, i.e. we'd like $(x,y)=x-y$.  Notice however that the right side does  not mention − in any way, it just uses existing properties of $(\R,+)$.
In order to operate like a difference, i.e. $(x-y)+(x'-y') = (x+x') - (y+y')$, we notice that $x-y = (x+a)-(y+a)$ for any $a$. The equivalence relation will fix the ambiguity and implicitly introduce the properties of −
$$\def\~{\sim} (x,y) \~ (x',y') \quad\iff\quad x+y' = x'+y$$
Again, only features of $(\R,+)$ are used. Then consider the equivalence classes $R=(K,+)/\!\~$ and show:


*

*The definition + is is well defined in $R$, i.e. for any $k,k', q, q'$ in $K$ there is $$ k\~k' \;\land\; q\~q'\quad\implies\quad k+q \~ k'+q' $$
This means the result of $r+q$ is independent of which representative we chose for $r$ or $q$.

*$(R,+)$ (and $(K,+)$ for that matter) inherits properties from $(\R,+)$ like: + is closed, associative and kommutative.

*For any $x,y,z\in\R$ we have
$$(x,y) + (z,z) = (x+z,y+z) \~ (x,y)$$
Thus $(z,z)$ operates as neutral element and we write $0_R:=(1,1)\~(z,z)\in\ R$.

*For any $x,y\in\R$ we have
$$ (x+1,1) + (y+1,1) = (x+y+2, 2)\~(x+y+1, 1)$$
This means the elements of the form $(x+1,1)$ operate under addition exactly the same like the elements of $\R$ do; "$(x+1,1)$" or "$(x+a,a)$" are just fancy ways to write "$x$".  This means the subset is isomorphic to $(\R,+)$:
$$\left(\{(x+y,y)\in \R\!\x\R \}{\large/}\!\~,+\right) \;\simeq\; (\R,+)$$
This in turn means

$R$ is actually an extension of $\R$: It contains an isomorphic copy of $(\R,+)$ and also new elements like $0_R=(1,1)$ that cannot be interpreted as element of $\R$.


*Observe that $(x,y)+(y,x) = (x+y,x+y)\~(1,1)=0_R$. This means $R$ has a neutral element $0_R$ and each element $(x,y)$ of $R$ has an additive inverse $(y,x)$.

Hence $(R,+)$ is a group.


*We write:
$$-(x,y) := (y,x)\quad\text{ and }\quad(x,y)-(x',y') := (x,y)+(y',x')$$

*Proceed in the same way for a multiplication provided we already have $\def\.{\cdot} (\R,+,\.)$: Define, now with $K=(\R,+,\.)\x(\R,+,\.)$
\begin{align}
\cdot :K\x K&\to K \\
(x,y) \cdot (x',y') &\mapsto (x\.x'+y\.y', x\.y'+x'\.y)
\end{align}
Again, show it's well defined when applying ~, notice that it inherits closedness, associativity, kommutativity, distributivity from $K$.

*Notice $(x,y)\.(2,1) = (2x+y, 2y+x)\~(x+y)$ and hence we have a One $1_R\~(2,1)$ in $R$. And the same embedding like above still applies because
$$(x+1,1)\.(y+1,1)=((x+1)(y+1)+1,x+y+2)\~(xy+1,1)$$
So $(K/\!\~,+,\.)$ is an extension of $(\R,+,\.)$.
You got the idea. You can proceed the same way for division, or if you don't have division yet define it similar and factor out that $x/y = (ax)/(ay)$.  The only thing is to keep in mind that zero is special.
Likewise, relations like $=$, $\neq$, $<$, $\leqslant$, $>$, $\geqslant$ can be carried over, some of them with restrictions. For example
$$x>y \iff z\.x > z\.y$$
for $x,y,z\in\R$, but monotony in $R$ only holds true if $z>0$.
The final step is then to identify $\R$ with it's isomorphic embedding in $R$ and use the notation $\Bbb R := R$ calling the equivalence classes Real numbers (again).

Note: The notation above is somewhat sloppy as it uses the same notation $(x,y)$ for elements of $\R\x\R$ and equivalence classes modulo ~ for brevity. More strict notation would be using $$R\ni\overline{(x,y)}:=\{(x',y')\in K \mid (x,y)\~(x',y')\}\subseteq K$$
