3

Let the real numbers and the relations =, >, $\ge$ be defined as in this lecture PDF.

I want to show the following statement:

$$\forall x \in \mathbb{R}( x \ge 0 \wedge x \neq 0 \Longrightarrow x > 0).$$

From $ x \ge 0$ we get that for all $(q,q') \in x$ and $(r,r') \in 0$ the following holds: \begin{align*} r \le q'. \end{align*} From we $ x \neq 0$ we get that there exists $(u,u') \in x $ and $(v,v') \in 0$ such that $[u,u'] \cap [v,v']$ have no rational point in common. $\underline{\text{This implies } v' < u}$; whence $ 0 < x$.

I am not sure wether the underlined part is true.

gt6989b
  • 54,422
  • If you give the link to the pdf, at least say were to look for the definitions – Jakobian Jun 18 '18 at 15:17
  • @Adam Unfortunately, the link does not have enumerated pages, but I would say that the definitions are slightly after the after the half of the paper. The chapter is called "the real line". –  Jun 18 '18 at 15:21
  • Every pdf does, look again. For anyone wondering, it's page 56 – Jakobian Jun 18 '18 at 15:23
  • @Adam If you click on the link, you can't see that it doesn't. At least I can't see them. If you search for the chapter, you will immediately find the definitions. –  Jun 18 '18 at 15:24
  • 1
    From $x \not = 0$ we have a rational interval $[a,b]$ containing $x$ and disjoint from $0$. If the interval is to the left of $0$, we have a contradiction with $x \geq 0$, from which we can obtain the conclusion. If the interval is to the right of $0$, then we see $x > 0$. – Carl Mummert Jun 18 '18 at 15:24
  • The definitions seem to start on p. 56 of the slides. Crucially, these slides write $x \not = 0$ for $x # 0$ ($x$ and 0 are separated) rather than $\lnot (x = 0)$ (x is not equal to zero). – Carl Mummert Jun 18 '18 at 15:26
  • @Carl But isn't the step "interval to the left of 0 -> contradiction, hence to the right" using the law of excluded middle? –  Jun 18 '18 at 15:32
  • 1
    No, it uses the inference rule $\bot \to \phi$, which is constructively acceptable. Another way of looking at it is that for rational $q$ we have $q < 0 \lor q = 0 \lor q > 0$, and so we can reason constructively about those three possibilities using excluded middle. To put this in the language of your sketch, you know that $u' < v \lor v' < u$, and in either case you can prove $x > 0$. In the case $v' < u$ this is immediate, and in the case $u' < v$ it follows from the proof by contradiction rule, because it gives $\lnot (0 \leq x)$. – Carl Mummert Jun 18 '18 at 15:33
  • Maybe a better way of writing the inference rule for this case is: $[(A \lor B) \land \lnot A] \to B$. This is constructively justified as: if I know I have a proof of A or I know I have a proof of B, and I know I do not have a proof of A, then I know I have a proof of B. – Carl Mummert Jun 18 '18 at 15:43
  • @Carl Thanks. Maybe as a follow up question: Is it possible to show $ x \ge 0 \wedge \neg (x = 0) \Rightarrow x > 0$?. –  Jun 18 '18 at 16:25
  • isn't this what your question asks? – Kenny Lau Jun 18 '18 at 16:26
  • @Kenny No, there is a difference between $ x \neq 0$ and $ \neg ( x= 0)$. –  Jun 18 '18 at 16:31
  • Hmm, to me, the construction given has a striking resemblance to the construction via filters – Kenny Lau Jun 18 '18 at 16:35
  • @Diamir I doubt its possibility. $x > 0$ is an existence, $x \ge 0$ is a forall, $\neg(x=0)$ doesn't give you any data, so you're trying to construct something from nothing. – Kenny Lau Jun 18 '18 at 16:38
  • Doesn't that imply Markov's principle (P.55)? – Kenny Lau Jun 18 '18 at 16:39
  • 1
    @kenny I think you are right, it might even be equivalent to MP. –  Jun 18 '18 at 16:41

1 Answers1

1

The problem is that you have to justify From $x \neq 0$ we get that there exists $(u,u′) \in x$ and $(v,v′) \in 0$ such that $[u,u′] \cap [v,v′]$ have no rational point in common. as this is not an axiom used in your document for the construction of $\mathbb R$.

Let's do it.

By definition of $x \ge 0$, for all $(q,q^\prime) \in x$ you have $q^\prime \ge 0$, see page 59. This is also a consequence that the rational number $0$ is canonically identified as $\{(0,0)\}$, see page 57.

Now as $x \neq 0$, by page 58, you must have $(q,q^\prime) \cap \{0\} = \emptyset$. And this enables to conclude that $q > 0$ and therefore to $x >0$ using again page 58.

The important topic is that for a rational number $q$, the "associated" real number is the set $\{(q,q)\}$ as stated in page 57. In that case the "associated real number" contains a single ordered pair!

mathcounterexamples.net
  • 70,018