Translating Tarski's Axiomatization/Logic of $\mathbb R$ to the Theory of Magnitudes

A little Euclid [1] helps; so if, for the purposes of this project, you "threw away all your math books", at least retrieve that one! :)

The proposition can be proved from P-0 to P-4 and the Archimedean property; completeness (P-5) is only used to prove the latter, and denseness (P-4) is not needed at all. (Of course, P-4 and P-5 are both needed for characterising $\mathbb{R}_{>0}$, or complete systems of magnitudes in general.)

It is clear from the definition of the order relation in $M$, in conjunction with the axioms of associativity and commutativity, that addition respects order: that is, if $x < y$, then $w + x < w + y$, and so on.

For present purposes, I'll take $\mathbb{N}$ to be the set of positive integers, i.e. zero is excluded. I'll take for granted the usual properties of $\mathbb{N}$, as well as the binary operation $\mathbb{N} \times M \to M$, $(n, x) \mapsto nx$, defined recursively in the usual way for semigroups. In particular, $1x = x$, $m(nx) = (mn)x$, $(m + n)x = mx + nx$, and because of the commutativity of addition in $M$, $n(x + y) = nx + ny$, for all $x, y \in M$ and $m, n \in \mathbb{N}$. (Thus, the map $M \to M$, $x \mapsto nx$ is an endomorphism of $M$.)

If $x < y$, then by definition there exists $u$ with $x + u = y$, so $nx + nu = ny$, so $nx < ny$. If $m < n$, then there exists $p \in \mathbb{N}$ with $m + p = n$, so $mx + px = nx$, so $mx < nx$. Similarly $mx > nx$ if $m > n$; so we have $m < n$ or $m = n$ or $m > n$ according as $mx < nx$ or $mx = nx$ or $mx > nx$.

By induction on $n$, if $x < y$, then $nx < ny$, and if $x > y$, then $nx > ny$; so we have $x < y$ or $x = y$ or $x > y$ according as $nx < ny$ or $nx = ny$ or $nx > ny$. Thus we can "divide by $n$" when handling inequalities or equations in $M$.

For $x, y \in M$, define the ratio of $x$ to $y$ to be the binary relation on $\mathbb{N}$, $$ x \mathbin{:} y = \{ (n, m) : nx > my \}. $$

^{Under a more general definition of a system of magnitudes,
$\mathbb{N}$ itself is a system of magnitudes, Archimedean, but not
complete. One can define the rational number $\tfrac{m}{n}$ as the
ratio $m \mathbin{:} n$ in that system. Then one can prove
that the set of all ratios is totally ordered by inclusion. Under a
still more general definition, in which the order relation is given
as a primitive concept instead of being defined in terms of addition,
the set of integers $> 1$ is a system of magnitudes, also Archimedean,
and also not complete, having multiplication as its "addition"
operation. One can can define $\log_nm$ as the ratio $m \mathbin{:} n$
in that system. Incidentally, one need not even have an operation of
addition of magnitudes. See section 3.10.1, "Extensive Multiples",
in Krantz et al. [2] I won't pursue any of these thoughts further here,
because they lead far afield! I develop only enough theory to prove
that any two endomorphisms of $M$ commute.
But if you have an appetite for more, and
can get hold of Scott's unpublished notes [3]: he develops a theory along
quite similar lines. His approach is not the only one possible. For
instance, one can characterise those binary relations on $\mathbb{N}$
that are ratios, without initially referring to systems of magnitudes
at all, and then prove that ratios form a complete system of
magnitudes. But I found that that approach gets a bit messy, or at
least in my hands it does! Please excuse this digression.}

Lemma 1 For all $x, y \in M$, and for all $r \in \mathbb{N}$, $$ x \mathbin{:} y = (rx) \mathbin{:} (ry). $$

Proof \begin{align*} x \mathbin{:} y & = \{ (n, m) : nx > my \} && \text{by definition} \\ & = \{ (n, m) : r(nx) > r(my) \} && \text{by ``division by $r$'' (see above)} \\ & = \{ (n, m) : (rn)x > (rm)y \} \\ & = \{ (n, m) : (nr)x > (mr)y \} \\ & = \{ (n, m) : n(rx) > m(ry) \} \\ & = (rx) \mathbin{:} (ry) && \text{by definition.} \end{align*} $\square$

Proposition 2 For systems of magnitudes $M, N$, $x, y \in M$, $u, v \in N$, and $p, q \in \mathbb{N}$, $$ \text{if } x \mathbin{:} y = u \mathbin{:} v, \text{ then } (px) \mathbin{:} (qy) = (pu) \mathbin{:} (qv). $$

Proof \begin{align*} (px) \mathbin{:} (qy) & = \{ (n, m) : n(px) > m(qy) \} && \text{by definition} \\ & = \{ (n, m) : (np)x > (mq)y \} \\ & = \{ (n, m) : (np)u > (mq)v \} && \text{because } x \mathbin{:} y = u \mathbin{:} v \\ & = \{ (n, m) : n(pu) > m(qv) \} \\ & = (pu) \mathbin{:} (qv) && \text{by definition.} \end{align*} $\square$

^{This is another of Euclid's results. It can be used to define
multiplication of ratios in general by rational numbers in
particular. We don't actually need it, but I thought I'd throw it
in anyway. So sue me. :)}

Lemma 3 For all $x, y, u \in M$, if $x < y$, then there exist $n, m \in \mathbb{N}$ such that $nx < mu < ny$.

Proof By hypothesis, there exists $t$ such that $y = x + t$. By the Archimedean property (as proved in the question, or postulated without also postulating completeness), there exists $n \in \mathbb{N}$ such that $nt > u$. Hence: $$ ny = nx + nt > nx + u. $$ Again by the Archimedean property, there exists $m \in \mathbb{N}$ such that $mu > nx$. Let $m$ be the smallest integer satisfying this condition. If $m = 1$, then $$ nx < u < ny. $$ On the other hand, if $m > 1$, then by the definition of $m$, $(m - 1)u \leqslant nx$. Therefore, $$ mu = [(m - 1) + 1]u = (m - 1)u + u \leqslant nx + u < ny, $$ as required. $\square$

Corollary 4 For all $x, y, u \in M$, if $x \mathbin{:} u = y \mathbin{:} u$, then $x = y$.

Proof If $x \ne y$, then $x < y$ or $x > y$. Supposing that $x < y$, the lemma implies that $(n, m) \in y \mathbin{:} u$ but $(n, m) \notin x \mathbin{:} u$, therefore $x \mathbin{:} u \ne y \mathbin{:} u$. Similarly if $x > y$. $\square$

Corollary 5 For all $x, y, u \in M$, if $x \mathbin{:} u = x \mathbin{:} v$, then $u = v$.

Proof If $u \ne v$, then $u < v$ or $u > v$. If $u < v$, then by applying the lemma to $u, v, x$, instead of $x, y, u$, we find that there are $n, m \in \mathbb{N}$ such that $$ mu < nx < mv, $$ so $(n, m) \in x \mathbin{:} u$ but $(n, m) \notin x \mathbin{:} v$, so $x \mathbin{:} u \ne x \mathbin{:} v$. Similarly if $u > v$. $\square$

Corollary 6 For all $x, y, u, v \in M$, if $x \mathbin{:} u = y \mathbin{:} v$, then $x < y$ or $x = y$ or $x > y$ according as $u < v$ or $u = v$ or $u > v$.

Proof The previous corollary has dealt with the case $x = y$. If $x < y$, take $n, m$ as in the lemma. Because $x \mathbin{:} u = y \mathbin{:} v$ and $nx < mu$, we have $(n, m) \notin y \mathbin{:} v$, i.e. $ny \leqslant mv$, whence $mu < mv$, whence on "dividing by $m$", $u < v$. Interchanging the roles of $x$ and $y$, and of $u$ and $v$, in this argument, we find that if $x > y$ then $u > v$. $\square$

Theorem 7 For all $x, y, u, v \in M$, $x \mathbin{:} y = u \mathbin{:} v$ if and only if $x \mathbin{:} u = y \mathbin{:} v$.

Proof By the symmetry of the result, we need only prove that if $x \mathbin{:} y = u \mathbin{:} v$ then $x \mathbin{:} u = y \mathbin{:} v$. If $x \mathbin{:} y = u \mathbin{:} v$, then for all $n, m \in \mathbb{N}$, by two applications of Lemma 1, we have $(nx) \mathbin{:} (ny) = (mu) \mathbin{:} (mv)$. By Corollary 6, therefore: $nx < mu$ or $nx = mu$ or $nx > mu$ according as $ny < mv$ or $ny = mv$ or $ny > mv$; and in particular $x \mathbin{:} u = y \mathbin{:} v$. $\square$

^{This proof shines as brightly now as when Euclid
gave it two and half thousand years ago. (Unless I've managed to
tarnish it, that is! I haven't been closely following the sources
listed, or even my own old notes, having been more in the mood to work
things out as I went along, even at the risk of messing up.)}

It is clear that if $M, N$ are systems of magnitudes, and $\phi: M \to N$ is a morphism of semigroups, then $\phi$ respects the order structures of $M, N$, and is injective. It follows immediately that: \begin{equation} \tag{1}\label{eq:1} \phi(x) \mathbin{:} \phi(y) = x \mathbin{:} y \text{ for all } x, y \in M. \end{equation} If $N = M$, Theorem 7 gives the corollary: \begin{equation} \tag{2}\label{eq:2} \phi(x) \mathbin{:} x = \phi(y) \mathbin{:} y \text{ for all } x, y \in M. \end{equation} If $\psi: M \to M$ is also a morphism, taking $y = \psi(x)$ in \eqref{eq:2} and using \eqref{eq:1} gives: $$ \phi(\psi(x)) \mathbin{:} \psi(x) = \phi(x) \mathbin{:} x = \psi(\phi(x)) \mathbin{:} \psi(x), $$ and Corollary 4 gives $\phi(\psi(x)) = \psi(\phi(x))$. Because $x$ was arbitrary, it follows that $\phi \circ \psi = \psi \circ \phi$. $\square$.