Proof verification in constructive analysis

Question

I want to proof something in constructive analysis, that means without the law of excluded middle (or, if one prefers this interpretation, in intuitionistic logic).

First some definitions:

$C(x_1,x_2) = \{ \sum_{i=1}^{2} \lambda_i x_i : \lambda_i \in [0,1]\wedge \lambda_1 + \lambda_2 = 1 \}$.

A metric is the same as in "standard" analysis.

For some subset $Y$ of a metric space $X$ we define the distance from $x \in X$ to $Y$ by $d(x,Y) = \inf \{d(x,y) : y \in Y \}$.

Now the problem: I have a real number $\neg(x=0)$ and define the vectors $x_1 = (1,x)$ and $x_2 = (x,0)$ in $\mathbb{R}^2$. I want to show that $\neg(0= d(0,C(x_1,x_2))$.

To this end I want to use the following rule: If under the hypothesis of $b$ the statements $a$ and $\neg a$ both lead to $\bot$, then I get $\neg b$ (this does hold in intuitionistic logic). So I assume $0= d(0,C(x_1,x_2) = \inf \{d(0,\lambda x_1 + (1-\lambda)x_2 : \lambda \in [0,1] \} $. Let $\lambda_n$ be a sequence such that in the limit we attain the infimum above. Then I have two cases: i) $\lambda_n \rightarrow 0$ or ii) $\lambda_n \rightarrow t \in (0,1]$. In the first case is get $0 = \lim_{n\rightarrow \infty}d(0,\lambda_n x_1 + (1-\lambda_n) x_2) = d(0, x_2) $ and thus $x_2 = 0$, hence $x = 0$; a contradiction. In the latter case I get $0 = \lim_{n\rightarrow \infty}d(0,\lambda_n x_1 + (1-\lambda_n) x_2) = d(0,t x_1 + (1-t) x_2 )= d(0,t(1,x) + t(x,0))$. In particular $tx = 0$, a contradiction. In total I get the desired result.

Inter alia I have the following questions: Can I define such a sequence $\lambda_n$?. Can i conclude constructively from $tx= 0$ that either $t = 0$ or $x =0$?. Thanks in advance.

Answer 1

I think I can answer the following problem: $xy = 0$ then either $x = 0$ or $y = 0$. First some definitions:

A real number is a subset x of $\mathbb{Q} \times \mathbb{Q}$ such that

i) for all $(q,q')$ in $x$ we have $ q \le q'$,

ii) for all $(q,q')$ and $(r,r')$ in $x$, the closed intervals $[q,q']$ and $[r,r']$ in $\mathbb{Q}$ intersect in points in $\mathbb{Q}$,

iii) for all positive rational $\varepsilon$ there exits $(q,q')$ in $x$ such that $ q' - q < \varepsilon$.

We say that two real numbers $x$ and $y$ are equal if for all $(q,q') \in x $ and all $(r,r') \in y$ the closed intervals $[q,q']$ and $[r,r']$ have a rational point in common.

The product $xy$ is defined to be the set of all rational pairs $(s,s')$ such that there exists $ (q,q') \in x$ and $(r,r') \in y$ with \begin{align*} s = \min\left\{qr,qr',q'r,q'r'\right\}, \quad s' = \max\left\{qr,qr',q'r,q'r'\right\}. \end{align*}

Now to the problem: First notice that case distinction is allowed when considering rational numbers.

Let $(q,q') \in x$ and $(r,r') \in y$. Choose $(0,0) \in 0$. Set $s = \min\left\{qr,qr',q'r,q'r'\right\}$ and $s' = \max\left\{qr,qr',q'r,q'r'\right\}$. Let $(u,u') \in 0$. By definition we get $ u \le 0 \le u'$ and thus $0 \in [u,u']$. It now suffices to show $0 \in [q,q']$ or $0 \in [r,r']$. Notice first that we are not going to consider cases where $q > q'$ or $r > r'$, since this is not possible due to the definition. By assumption we have $ 0 \in [s,s']$.

Case 1(there exists an element $a \in \left\{qr,qr',q'r,q'r'\right\}$ such that $a = 0$): w.l.o.g assume $a = qr$. By this we get either $q = 0$ or $r = 0$. In the first case we get $ 0 \in [q,q']$ and in the latter we get $ 0 \in [r,r']$.

Case 2(there exist elements $a,b \in \left\{qr,qr',q'r,q'r'\right\}$ such that $a < 0 < b$).

Case 2.1($a = qr$ and $b = q'r$): by this we get $q < 0$ and $r > 0$. Therefore $q' > 0$ and thus $0 \in [q,q']$.

Case 2.2($a = qr$ and $b = q'r'$).

Case 2.2.1($q < 0$ and $r > 0$): then we get $r' > 0$ and thus $ 0 \in [r,r']$.

Case 2.2.2($q > 0$ and $r < 0$): then we get $q' > 0$ and thus $ 0 \in [q,q']$.

Case 2.3($a = q'r$ and $b = qr'$): this implies $q' > 0$ and $r < 0$.

Case 2.3.1($q >0$ and $r '> 0$): then we get $ 0 \in [r,r']$.

Case 2.3.2($q < 0$ and $r ' < 0$): then we get $ 0 \in [q,q']$.

Answer 2

I need to read your post more carefully which I shall do tomorrow. Are you reading about constructive analysis from a certain textbook?

I do know that the statement $\forall x,y \in \mathbb R \left(xy = 0 \implies \left(x=0 \lor y=0\right)\right)$ is equivalent to the lesser limited principle of omniscience (LLPO) which is known be nonconstructive (but weaker than LEM). I will prove the relevant (forward) direction of this aforementioned equivalence tomorrow.

---

Lesser limited principle of omniscience (LLPO): For each binary sequence $\{a_n\}_{n=1}^\infty$ with at most one term equal to $1$, either $a_{2n-1}=0$ for all $n$ or else $a_{2n}=0$ for all $n$.

---

Suppose that the statement $\forall x,y \in \mathbb R \left(xy = 0 \implies \left(x=0 \lor y=0\right)\right)$ holds. Let $\{a_n\}_{n=1}^\infty$ be a binary sequence with at most one term equal to $1$. We define two sequences $\{x_n\}_{n=1}^\infty$ and $\{y_n\}_{n=1}^\infty$ by \begin{equation}x_n:= \begin{cases} \frac{1}{k} & \text{ if } \, 2k-1 \leq n \text{ and } \, a_{2k-1}=1, \\ 0 & \text{ otherwise} \end{cases} \end{equation} and \begin{equation}y_n:= \begin{cases} \frac{1}{k} & \text{ if } \, 2k \leq n \text{ and } \, a_{2k}=1, \\ 0 & \text{ otherwise}. \end{cases} \end{equation} Put $x=\lim_{n \to \infty} x_n$ and $y=\lim_{n \to \infty} y_n$. Notice $xy=0$, since $x_ny_n = 0$ for every $n \in \mathbb N$. Furthermore, $x=0$ iff $a_{2n-1}=0$ for all $n$, and $y=0$ iff $a_{2n}=0$ for all $n$.

Answer 3

I think I found the answer: my proof has some flaws, in particular such a sequence can not be defined constructively. However, I did come up with the following proof:

Assume
\begin{align}\label{eq11} 0=d(0,C(a_1,a_2)). \end{align} We call this equation * . Notice that $d(0,C(a_1,a_2)) = \inf \{d(0,\lambda a_1 + (1-\lambda)a_2) : \lambda \in [0,1]\}$. We are going to show that (*) implies $x=0$, which would contradict $\neg(x=0)$. Assume that $\vert x \vert > 0$. We have two cases:

Case 1 $(x > 0)$: we have either $\lambda > 1/2$ or $ \lambda < 2/3$. In the first case we obtain $ \lambda + (1-\lambda)x > 1/2 > 0$ and in the latter case $\lambda + (1-\lambda) x > x/3 > 0$. Therefore both contradict (*).

Case 2 $(x < 0)$: we may assume $\vert x \vert < 1/2$. We have either $\lambda > -x /3$ or $\lambda < -x/2$. In the first case we get $\lambda x < - x^2/3 < 0$. In the latter case we obtain $ \lambda + (1-\lambda)x < \lambda +x/2 < 0$. Therefore both contradict (*).

In total we observe $x =0$. Thus $(*)$ implies $\bot$, i.e. we get $\neg(0=d(0,C(a_1,a_2))$.