I am a PhD student currently studying for an upcoming analysis test. I was working through some problems with a study group and one problem was to show that functions with a certain property send sets of measure zero to sets of measure zero. With the property, it was very easy to show that for any set of measure zero, the measure of the image is smaller than any positive number. I said "We can use a quick contradiction to get the result" and a friend of mine said "why would you do contradiction when you can show it directly?"
Her reasoning was that if a non-negative number is smaller than any positive number, it is clearly zero. I definitely agree with this, but I don't see a way to actually prove it without deriving a contradiction. So, my question is, does anyone know a constructivist proof of the fact that a non-negative number that is smaller than any positive number is zero?
Many systems of constructive analysis reject the classical axiom: $$ (\forall x \in \mathbb{R})[x < 0 \lor x = 0 \lor x > 0].\qquad\qquad\qquad (*) $$ Intuitively, this rejection comes from the fact that, in general, there is no way to decide, given an $x \in \mathbb{R}$, which of the three alternatives holds. However, the analogous formula to $(*)$ for $\mathbb{Q}$ is constructively acceptable, because given a fraction we can tell which option holds by inspection.
There are some systems of constructive analysis which are compatible with the existence of infinitesimals. In such systems, the axiom above will really fail to hold, and the result from the question will not be provable.
However, there are some constructive systems where you can prove the result from the question, which is $$ (\forall x \in \mathbb{R})[x \geq 0 \land (\forall r \in \mathbb{Q}^+)[x \leq r] \to x = 0].\qquad\qquad\qquad (**) $$ Unfortunately, work in constructive mathematics requires careful attention to the definitions of "real number" and the order relations on the reals. Different constructive system define these in different ways which affect the theorems that can be proved.
In the systems I have in mind, a real number is defined to be a quickly converging Cauchy sequence of rationals, that is, a sequence $(x_n)$ of rationals such that $|x_n - x_m| \leq 2^{n}$ when $n < m$. The relation $x \leq y$ is defined as $$ (\forall k)[x_k \leq y_k - 2^{-k+1}], $$ and $x = y$ is defined as $x \leq y \land y \leq x$. The real number $0$ is defined as the constant Cauchy sequence made from $0_\mathbb{Q}$, and the same method is used to embed $\mathbb{Q}$ into $\mathbb{R}$. These definitions, for example, are compatible with Bishop's system for constructive analysis.
In such systems, we can prove (**) without the law of the excluded middle (but using the fact that (*) holds for $\mathbb{Q}$).
To do so, we already have $0 \leq x$, by assumption, so we need to prove $x \leq 0$ and we are done. This means we need to prove that $(\forall k)[x_k \leq -2^{-k+1}]$.
For each rational $r$, we already know that $x \leq r$. In particular we know $(\forall r > 0)(\forall k)[x_k \leq r - 2^{-k+1}]$. Now we fix $k$ and apply (*) in the form of the proposition $$ x_k < -2^{-k+1} \lor x_k = -2^{-k+1} \lor x_k > -2^{-k+1}. $$ The disjunction here is decidable, because $x_k$ is an explicit rational. And we can prove that $x_k > -2^{-k+1}$ is impossible because, if it happens, then we can write (constructively) $x_k = s + -2^{-k+1}$, and then let $r = s/2$ and we will have $x_k > r - 2^{-k+1}$, which is impossible because we know that $x \leq r$ in the sense of $\mathbb{R}$.
Now, although excluded middle is not provable constructively, the following tautology is provable constructively: $$ (A \lor B \lor C) \land (\lnot C) \to (A \lor B). $$ In our case, that means that we can prove $(x_k < 2^{-k+1} \lor x_k = 2^{-k+1})$ for all $k$. Which is exactly what we need to prove to show that $x \leq 0$ in the sense of $\mathbb{R}$, completing the proof of $(**)$.