1

From Bishop's constructive analysis book I know for some real numbers $x$ and $y$ at most one of the statements $x=y$, $x \ne y$ is true.

Can I also show constructively that exactly one of the statements is true (i.e. a need to show that at least one of the statements is true)? My intuition says this is not possible since this would be some kind of a $A\vee\lnot A$ statement.

Karn Watcharasupat
  • 4,323
  • 1
    $x\neq y$ is basically an abbreviation of $\lnot(x=y)$, so I'd say you're right. – Arthur Apr 30 '18 at 15:44
  • 1
    Ok. Am I allowed from a constructive point of view to proof some with the following way: Case 1) $x \ne y$ and then show the statement. Case 2) $x = y$ and then show the statement. –  Apr 30 '18 at 16:48
  • The reals are an ordered field. Maybe you can make use of the fact that either $x > y$, $x < y$ or $x = y$. I am not sure if you can prove this constructively, though, however, some axiomatizations even list this as an axiom. – ComFreek Apr 30 '18 at 17:22
  • @Diamir You could then conclude $(x = y \implies S) \wedge (\neg (x = y) \implies S)$ where $S = (x = y) \vee \neg (x = y)$. But that doesn't help you generally $(A \implies B) \wedge (\neg A \implies B) \implies B$ would be equivalent to $A \vee \neg A$. (You can easily see this if you set $B := A \vee \neg A$.) – ComFreek Apr 30 '18 at 17:25
  • Yes, but this fact is the so called LPO which is, as you said, an axiom. However, I want to work in the framework of LLPO which only states $x \ge y$ $\vee$ $x \le y$. –  Apr 30 '18 at 17:31
  • No. In total I want to show that the statement: $\exists \xi \in \mathbb{R}^{1 \times m} : \xi * A > 0 \Leftrightarrow \neg \exists p \in { x \in \mathbb{R}^{n \times 1} : x_i > 0 \wedge x_1 + ... + x_n =1} : A*p= 0$, where $ A \in \mathbb{R}^{ m \times n}$ implies the LLPO. –  Apr 30 '18 at 17:54

0 Answers0