# How to solve $(x-1)(x-2)=0$ constructively?

I want to prove that

$$(x-1)(x-2)=0\Leftrightarrow x=1, 2$$

$$\Leftarrow$$ is easy. The problem is $$\Rightarrow$$.

Assuming $$x\neq 1, 2$$, we can derive $$1=0$$ by dividing both sides of $$(x-1)(x-2)=0$$ by $$x-1$$ and $$x-2$$.

Thus we get $$\lnot \lnot (x=1, 2)$$. However, intuitionistic logic cannot eliminate double negation.

• After posting the question, I realized that it seems that it is not possible to solve it constructively because I lack the information to determine whether $x$ is $1$ or $2$. May 28 at 7:05
• What is your intended domain here? Integers? Rationals? Dedekind reals?
– S.C.
May 28 at 7:12
• @S.C. It is real numbers. I do not know what the Dedekind reals are. May 28 at 7:15
• In a generic constructive context, there's a difference between reals as given by Cauchy sequences and reals as given by Dedekind cuts. It might not matter for this question, but you never know.
– S.C.
May 28 at 7:18
• The statement $x=1,2$ is too ambiguous for something as precise as a constructive proof. As you said, if you take it to mean $x = 1 \lor x = 2$ then there probably is no constructive proof, although that's not guaranteed since you could have an axiom that has similar strength to what induction does for natural numbers. E.g., if you restricted your domain to naturals then the lack of a tag on the disjunction isn't an obstacle because naturals are enumerable, and most axioms sets would reflect that. May 28 at 7:25

A useful construction on real numbers and more generally is that of a apartness relation. Such a relation is defined to be antireflexive, symmetric and cotransitive, meaning that if $$x \# z$$ then $$x \# y$$ or $$y \# z$$. Classically, this is just the negation of an equivalence relation. Additionally, a tight apartness relation satisfies $$\neg (x\ \#\ y) \Rightarrow x = y$$.

As you'll see proved in any book on constructive analysis, the real numbers have such a relation given by $$x$$ and $$y$$ are apart if there is a rational number between them, i.e., $$\exists q \in \mathbb{Q}\ (x < q \land q < y) \lor (y < q \land q < x)$$. You'll also find that if $$x \# 0$$, we can divide by $$x$$.

Now, given $$x\ \#\ y$$, we can prove that $$x y = 0$$ implies $$x = 0$$ or $$y = 0$$. This is fairly simple. Since $$x\ \#\ y$$, cotransitivity tells us that $$x\ \#\ 0$$ or $$y\ \#\ 0$$. In the first case, since we can divide by $$x$$, $$x y = 0 = x \cdot 0$$ implies that $$y = 0$$. Similarly, in the second case $$x = 0$$, so $$x = 0$$ or $$y = 0$$.

To apply this to your situation, we need to prove that $$(x - 1)\ \#\ (x - 2)$$. This seems pretty plausible, since the two numbers are pretty far apart. In fact, any good enough rational approximation of $$x - 3/2$$ will do.

To procure such a rational approximation, you need some details about which reals you're using. For Cauchy reals, this is trivial since a Cauchy real is equipped with a function that gives a rational approximation to that number with any given precision. We just need to take a rational $$q$$ within $$1/2$$ of $$x - 3/2$$ and that rational will be between $$x - 2$$ and $$x - 1$$. $$x - 3/2 - q < 1/2$$ implies $$x - 2 < q$$ and $$q - (x - 3/2) < 1/2$$ implies $$q < x - 1$$.

For Dedekind reals, we have to be a bit more creative. To start, a Dedekind cut is given by two sets $$L$$ and $$R$$ of rationals. They must both be inhabited (there exists an element of each). $$L$$ should be lower rounded, meaning that $$q$$ is in $$L$$ if and only if there is another rational $$r$$ in $$L$$ with $$q < r$$. Similarly, $$R$$ must be upper rounded. The cuts must be ordered: if $$q$$ is in $$L$$ and $$r$$ is in $$R$$, the $$q < r$$. Finally, the cuts must be located: if $$q < r$$, then either $$q$$ is in $$L$$ or $$r$$ is in $$R$$.

To get arbitrarily close rational approximations to a given Dedekind cut, we can use inhabitedness to get a starting point and locatedness to get a better rational approximation.

Let $$x = (L, R)$$ be a Dedekind cut and let $$\epsilon > 0$$ be some rational number. We want to find an interval with rational endpoints that both contains $$x$$ and has length less than $$\epsilon$$.

By inhabitedness, there exists $$q_0$$ in $$L$$ and $$r_0$$ in $$R$$. By the ordered property, $$q_0 < r_0$$, so $$r_0 - q_0 > 0$$. Let $$N$$ be positive integer such that $$(r_0 - q_0)/N < \epsilon$$.

Then divide $$(q_0, r_0)$$ into $$N$$ subintervals. Explicitly, let $$q_k = q_0 + k \cdot (r_0 - q_0)/N$$.

By the locatedness property, either $$q_k$$ is in $$L$$ or $$q_{k + 1}$$ is in $$R$$. Since $$q_0$$ is in $$L$$ and $$q_N = r_0$$ is in $$R$$, not all of the $$q_k$$ are in one set. Furthermore, if $$q_k$$ is in $$L$$, then $$q_i$$ is in $$L$$ too for $$i < k$$ and vice versa for $$R$$. This means that there is a unique $$n$$ such that $$q_n$$ is in $$L$$ and $$q_{n + 1}$$ is in $$R$$. Thus, $$(q_n, q_{n + 1})$$ is an interval of length $$(r_0 - q_0)/N < \epsilon$$ that contains $$x$$. Both $$q_n$$ or $$q_{n + 1}$$ are rational approximations within $$\epsilon$$ of $$x$$.

To apply this to our problem, we needed a rational strictly between $$x - 1$$ and $$x - 2$$. To get this, use a rational approximation of $$x - 3/2$$ that is accurate to (strictly) within $$\epsilon = 1/2$$.

Real numbers have a property called locatedness, which states that for all $$a, b, c$$ with $$a < b$$, we have $$a < c \lor c < b$$. Suppose $$(x - 1)(x - 2) = 0$$. Apply locatedness to $$a = 1$$ and $$b = 2$$ to conclude that either $$1 < x$$ or $$x < 2$$.

If $$1 < x$$, then $$0 < x - 1$$, so $$x - 1$$ has a multiplicative inverse. Therefore, $$x - 2 = 0$$, so $$x = 2$$.

If $$x < 2$$, then $$x - 2 < 0$$, so $$x - 2$$ has a multiplicative inverse. Therefore, $$x - 1 = 0$$, so $$x = 1$$.

Thus, either $$x = 1$$ or $$x = 2$$.

The second implication would follow if $$\neg (x=1 \wedge x=2)$$. This is equivalent to $$(x-1)\neq 0 \lor (x-2)\neq 0$$, and so: $$\neg (x=1\wedge x=2) \wedge (x-1)(x-2)=0$$ is equivalent to: $$((x-1)\neq 0 \wedge (x-1)(x-2)=0)\lor((x-2)\neq 0 \wedge (x-1)(x-2)=0)$$ which is equivalent to: $$((x-1)\neq 0 \wedge (x-2)=0)\lor((x-2)\neq 0 \wedge (x-1)=0)$$ In the first case, with the right and you get $$x=2$$, in the second you get $$x=1$$.

I do think the first claim can be proven constructively ($$x=1 \wedge x=2$$ implies $$1=2$$ which leads to contradiction, hence the negation holds). But please do correct me if i'm wrong (i'm fairly new to constructive thinking).

• Welcome to Math.SE! One can indeed establish constructively that $\neg (x = 1 \wedge x = 2)$ holds. But the very next step breaks: $\neg (x = 1) \vee \neg (x = 2)$ need not follow constructively from $\neg (x = 1 \wedge x = 2)$. May 28 at 11:13