constructive proof that $\mathbb{R}$ is an integral domain?

Question

Can it constructively be shown that for all $x,y \in \mathbb{R}$, $xy = 0 \rightarrow x = 0 \vee y = 0$?

e: The reason that I am interested in this is that I recall hearing something about how the roots of polynomials in a constructive setting aren't generally as nice as you would expect. For instance, for $\alpha \geq 0$ we can show that the polynomial $x^2 - \alpha$ does indeed factor as $(x-\sqrt\alpha)(x + \sqrt\alpha)$ but we cannot conclude that an arbitrary root $r$ is either $\sqrt\alpha$ or $-\sqrt\alpha$ without appealing to the integral domain property, which seems suspect for reals.

Answer 1

This is equivalent to the nonconstructive axiom, the lesser limited principle of omniscience (LLPO) (as long as we assume countable choice).

To show that $\mathbb{R}$ being an integral domain implies LLPO, let $\alpha \colon \mathbb{N} \rightarrow 2$ be an infinite binary sequence such that $\alpha(n) = 1$ at most once. To prove LLPO is to show that either $\alpha(2n) = 0$ for all $n$ or $\alpha(2n + 1) = 0$ for all $n$. Define $x := \sum_{n = 0}^\infty 2^{-\alpha(2n)}$ and $y := \sum_{n = 0}^\infty 2^{-\alpha(2n + 1)}$. Then $xy = 0$ (because for all $\epsilon > 0$ either $x < \epsilon$ or $y < \epsilon$ and certainly $x, y \leq 1$, so $xy < \epsilon$), but $x = 0$ implies $\alpha(2n) = 0$ for all $n$, and $y = 0$ implies $\alpha(2n + 1) = 0$ for all $n$.

To show that LLPO implies $\mathbb{R}$ is an integral domain, let $x, y$ be such that $xy = 0$. We construct a sequence $\alpha \colon \mathbb{N} \rightarrow 2$ as follows. For any $n$, if $\alpha(m) = 1$ for some $m < n$ take $\alpha(n)$ to be $0$. Otherwise split into cases depending on whether $n$ is even or odd. If $n$ is even, then either $x < 2^{-n}$ or $x > 2^{-n -1}$. Take $\alpha(n)$ to be $0$ if $x < 2^{-n}$ and $1$ if $x > 2^{-n -1}$. If both hold, $\alpha(n)$ can be either $0$ or $1$, so we need to use countable choice to pick a value. When $n$ is odd, we do the same but for $y$ instead of $x$. Then if $x = 0$ then $\alpha(2n) = 0$ for all $n$, and if $y = 0$ then $\alpha(2n + 1) = 0$ for all $n$.

Answer 2

I don't immediately see a good way to show how nonconstructive it is, but the principle $$ (\forall x,y \in \mathbb{R})[xy = 0 \to (x = 0 \lor y = 0)] $$ has no computable witness for the disjunction, and so it will not be constructively provable. Here I am taking $\mathbb{R}$ to be the set of quickly-converging Cauchy sequences of rationals, in the style of Bishop's Constructive Analysis.

In this situation, a computable witness for the disjunction is a (partial) function $F(x,y)$ so that if $x y= 0$ then $F(x,y) \in \{0,1\}$ and $F(x,y) = 0 \to x= 0$ and $F(x,y) = 1 \to y= 0$. In other words $F$ identifies one of two disjuncts which is true, in the case $xy = 0$. A general principle of constructive provability in this setting is that we would expect a computable witness to exist in this case if the formula were to be constructively provable. This is because a constructive proof of the overall principle would give us the algorithm needed to compute $F$.

The proof that there is no computable witness for the disjunction is by contradiction (we are using a classical proof to show that the original formula is not constructively provable.) Start by building both $x$ and $y$ as the sequence $1/2^n$. Because $F$ is computable, at some point it must return $0$ or $1$ just looking at long enough initial segments of $x$ and $y$. As soon as it does, we change the construction of whichever sequence $F$ selects ($x$ or $y$) so that this sequence becomes constant and nonzero. (If $F$ never returns $0$ or $1$ on the unmodified sequences $1/2^n$, we have a contradiction already.)

This process gives two computable sequences $x$ and $y$ so that $xy = 0$. However, $F$ does not select from $x$ and $y$ the sequence that converges to zero, and so we see there is no computable witness for the disjunction.

A "better" proof would show how nonconstructive the original principle is, rather than just showing that the principle is not constructively provable.