# Co-transitivity of the constructive order relation

One of the first exercises in J.L. Bell's A Primer of Infinitesimal Analysis asks the reader to show that, for arbitrary real numbers $a$, $b$, and $x$, if $a < b$, then either $x > a$ or $x < b$.

The reason this is not entirely trivial is that we're working in a constructive setting, one in which the law of the excluded middle does not hold. The goal is to prove the statement above from the axioms governing the strict ordering relation:

1. $a < b$ and $b <c$ implies $a < c$
2. $(a < a)$ is false
3. $a < b$ implies $a + c < b + c$
4. $a < b$ and $c > 0$ implies $ac < bc$
5. either $0 < a$ or $a < 1$
6. $a \neq b$ implies $a < b$ or $b < a$

Note that without the law of the excluded middle, we cannot establish the classical trichotomy that, for any two real numbers $x$ and $y$, one of $x < y$, $x = y$, or $x > y$ is true: it may still be the case that we cannot distinguish $x$ from $y$ sufficiently to establish any of these relations.

In Bell's presentation, we also know at this point that the real numbers with the operations of addition and multiplication form a field in the usual way, though with the caveat that in order to assume $x$ has a multiplicitive inverse we must know $x \neq 0$, a condition that is not automatic for numbers other than zero since we can't appeal to the law of the excluded middle.

Some Googling tells me that the statement to be proved is sometimes presented as a axiom (called co-transitivity) of constructive order relations. How can it be proved from Bell's axioms?

-
The conclusion in Axiom 3 should be $a+c<b+c$. –  Andreas Blass Jul 7 '13 at 0:33
"a condition that is not automatic for numbers other than zero since we can't appeal to the law of the excluded middle" - this isn't quite right. Looking at page 16, Bell defines $x \not = y$ to be $\lnot (x = y)$ so as soon as you know a number is other than zero you know it is $\not = 0$. What the lack of excluded middle says is that you can't assert $x = 0 \lor x \not = 0$; you can still assert $\lnot (x = 0) \to x \not = 0$. –  Carl Mummert Jul 18 '13 at 20:16
@Carl Mummert, yes, "as soon as you know a number is other than zero" you know $x \neq 0$, but you cannot reason by cases about an arbitrary number using the law of trichotomy, as you often would in a classical setting. So when you're considering an arbitrary quantity $x$, there's no way to get to $x \neq 0$. Right? –  pash Jul 18 '13 at 21:18
@pash: You cannot prove an arbitrary number is nonzero (of course) but in this system, if you know that $0 < x$ then you can prove $0 \not = x$ and so $1/x$ exists. So you can prove $x \not = 0$ when you have various other assumptions on $x$. The issue is that a number cannot be "other than zero" without being $\not = 0$. A number that is neither $= 0$ nor $\not = 0$ cannot be described as "other than zero" because, for all we know, it might turn out to be equal to zero once we get more information about it. –  Carl Mummert Jul 19 '13 at 11:53
@Carl Mummert, yes, that is my understanding, too. The caveat I gave was a poorly articulated attempt to clarify that, unlike in a classical setting, it is not the case in this field that only zero lacks a multiplicative inverse. ... And now I understand why constructivists had to come up with the notion of an apartness relation. –  pash Jul 19 '13 at 17:59

As a rule of thumb, in constructive mathematics often the way you prove a formula involving a disjunction is to start with an axiom which already has a disjunction. In this case notice that the only axioms mentioning disjunctions are 5 and 6. Also note that axiom 5 is kind of similar to what we have to prove, so that's the one we're going to use. It just needs a bit of adjusting.

First of all see that since $a < b$ we can apply axiom 3 to show that $0 < b - a$, so in particular we can divide by $b - a$.

Let $x' = \frac{x - a}{b - a}$. Now applying axiom 5 we know that either $0 < x'$ or $x' < 1$.

Suppose that $0 < x'$. Then by axiom 4 we can multiply through by $b - a$ (recall $0 < b - a$) to get $0 < x - a$, and then get $a < x$ by axiom 3.

Now suppose that $x' < 1$. Then multiplying through by $b - a$ again this time gives $x - a < b - a$. Then apply axiom 3 to get $x < b$.

But now we've shown that either $a < x$ or $x < b$ as required.

-
For the sale of dotting all the i's: Having that $0<b-a$ and wanting to divide by $b-a$, we invoke Axiom 2 to say $b-a\neq0$. –  Andreas Blass Jul 7 '13 at 0:35