It is stated by Douglas Bridges in Constructive mathematics: a foundation for computable analysis that the following property, which I will call the zero product property:
If $x,y \in \mathbb{R}$ and $xy = 0$, then $x = 0$ or $y = 0$.
is equivalent to the Lesser Limited Principle of Omniscience (LLPO):
For each binary sequence $(a_n)$ with at most one term equal to 1, either $a_{2n} = 0$ for all $n$ or else $a_{2n+1} = 0$ for all $n$.
The LLOP is non-algorithmic and a trivial consequence of the Law of Excluded Middle (LEM); as such it is often rejected by constructive mathematicians. In light of this revelation how do construcivists operate, in general situations, without use of the zero product property?
Best Answer
A common strategy in constructive mathematics is to define how to things can be different rather than just defining how things are the same.
Consider a local ring. One definition of a local ring is a ring where $0 \neq 1$ and where for all $x, y$, if $x + y = 1$ then either $x$ or $y$ is a unit. Equivalently, one can define a local ring to be one where $0$ is not a unit and where if $x + y$ is a unit, then either $x$ or $y$ is a unit.
In classical mathematics, one can equivalently characterize a local ring as a ring in which $\{(x, y) \mid x - y$ is not a unit$\}$ is an equivalence relation. This is a rather nice result because it provides a rather pithy description of a local ring.
In constructive logic, we actually want to flip this on its head.
An apartness relation $R \subseteq A^2$ is a relation satisfying three properties:
An equivalence relation on $A$ describes a sense in which two elements of $A$ can be said to be "the same". Conversely, an apartness relation on $A$ describes how two elements on $A$ can said to be "distinguishable".
Note that the complement $A^2 \setminus R$ of an apartness relation is an equivalence relation. In classical logic, an apartness relation is exactly the complement of an equivalence relation.
This suggests another definition of a local ring. A local ring is a ring where the relation $\{(x - y) \mid x - y$ is a unit$\}$ is an apartness relation.
This is the version that is constructively valid.
Clasically, one can further define a field to be a ring in which the relation $\{(x, y) \mid x - y$ is not a unit$\}$ is exactly the equality relation.
Constructively, the correct definition of a field is a local ring where the complement of the apartness relation $\# = \{(x, y) \mid x - y$ is a unit$\}$ is exactly the equality relation. An apartness relation whose negation is equality is known as a "tight apartness relation". We use $\#$ as a stronger version of $\neq$ - $\#$ is typographically similar to $\neq$.
The statement that an apartness relation is tight is the statement that if two elements cannot be distinguished using the given apartness relation, then they are identical.
We see that $x \# 0$ if and only if $x$ is a unit. Now suppose that $x \cdot y \# 0$. Then we see that $xy$ is a unit. Then both $x$ and $y$ are units. Then $x \# 0$ and $y \# 0$. In other words, if $xy$ is apart from $0$, then both $x$ and $y$ are apart from $0$.
Conversely, if $x \# 0$ and $y \# 0$, then both $x$ and $y$ are units; thus, $xy$ is a unit; and therefore, $xy \# 0$. So if $x$ and $y$ are both apart from $0$, then $xy$ is also apart from $0$.
Finally, let's suppose that $x$ and $y$ are distinguishable - that is, suppose that $x \# y$. Then either $x \# 0$ or $y \# 0$. If $x \# 0$ and $xy = 0$, then $\neg (xy \# 0)$; thus $\neg (y \# 0)$; thus, $y = 0$. And similarly, if $y \# 0$ then $x = 0$. So if $x \# y$ and $xy = 0$, then one of $x$ and $y$ is apart from $0$ and the other equals $0$.
We can still take advantage of most of the familiar theorems involving fields. In cases like $\mathbb{Q}$ where apartness is decidable, we have most of the power of classical linear algebra at our disposal.
It turns out that for the real numbers $\mathbb{R}$, we have $x \# y$ if and only if $x < y$ or $y < x$.
Apartness relations are also critical in topology. For example, the typical constructive definition of a Hausdorff space states that a space $X$ is Hausdorff if and only if $\{(x, y) \in X^2 \mid $ there are open sets $x \in U$, $y \in V$ such that $U \cap V = \emptyset\}$ is a tight apartness relation.