0

A real number is a subset $x$ of $\mathbb{Q} \times \mathbb{Q}$ such that for all $(q,q')$ in $x$ we have $ q \le q'$, and

a) 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}$,

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

The maximum of two real numbers $x$ and $y$ is defined by the set of all rational pairs of the form $(\max\{q,r\}, \max\{q',r'\})$, where $(q,q') \in x$ and $(r,r') \in y$ and f.e. $(\max\{q,r\}$ is the maximum in the real numbers.

Is the expression $r = \max\{x,y\}$ well defined? In my opinion yes, since I know that the maximum is again a real number. But doesn't this make the LLPO redundant?

LLPO: $\forall x \in \mathbb{R} (x \ge 0 \vee x \le 0)$.

For a detailed look at the definition of the real numbers c.f. this lecture PDF starting from page 56.

  • 1
    I don’t understand the link that you’re making between the question is the max well defined? and the redundancy with LLPO. By the way if you would have the kindness to define what LLPO means, that would be great! – mathcounterexamples.net Jun 26 '18 at 18:58
  • @mathcounterexamples.net LLPO is given at the bottom. Well if I can say that $\max{x,0} = 0$, then I know that $ x \le 0$ and similar for $x \ge 0$. –  Jun 26 '18 at 19:00
  • I meant what is the acronym LLPO standing for... I’m a bit old school and I don’t like to use words that I don’t understand. – mathcounterexamples.net Jun 26 '18 at 19:02
  • @mathcounterexamples.net Ah sorry, it means Lesser Limited Principle of Omniscience. –  Jun 26 '18 at 19:03
  • 2
    If you want to define a real number $\max{x,y}$ for real numbers $x,y$, then your definiens should be a real number. You present a pair of rationals (and a not well-defined such pair) instead of a set of pairs of rationals. - Also, with the supposedly definition of $<$ on your reals, it can happen that neither $x=y$ nor $x<y$ nor $x>y$ – Hagen von Eitzen Jun 26 '18 at 19:17
  • 1
    And I remember now! You asked this question about the construction of the reals you refer to... You were more generous at that time in providing the full view on the construction and not only the unsufficient fragment you provide here. – mathcounterexamples.net Jun 26 '18 at 19:24
  • @HagenvonEitzen I updated my post. –  Jun 26 '18 at 19:25
  • @mathcounterexamples.net You are absolutely right. Mea culpa. I will add this pdf to my post. –  Jun 26 '18 at 19:26

2 Answers2

1

The maximum function has the properties

$$x \max y < z \leftrightarrow x < z \wedge y < z$$

$$x < y \max z \leftrightarrow x < y \vee x < z$$

The converse of these properties is

$$x \max y \leq z \leftrightarrow x \leq z \wedge y \leq z$$

$$x \leq y \max z \leftarrow x \leq y \vee x \leq z$$

except

$$x \leq y \max z \rightarrow x \leq y \vee x \leq z$$

is not constructively provable. If it were, you could prove LLPO like so:

We have $x \max 0 \leq x \max 0$.

If $x \max 0 \leq x$, then $0 \leq x$.

If $x \max 0 \leq 0$, then $x \leq 0$.

0

Is the expression $s=\max\{x,y\}$ well defined?

Well, you have to validate that the axioms of definition of an element of $\mathbb R$ are fulfilled by $s$.

In particular for the first one that $\max\{q,r\} \le \max\{q^\prime, r^\prime$}, knowing that $q\le q^\prime $, $r \le r^\prime$ and that the closed intervals $[q,q']$ and $[r,r']$ in $\mathbb{Q}$ intersect in points in $\mathbb{Q}$. The last condition is fulfilled if and only if $q^\prime > r$ and $r^\prime >q$. The condition on the max is indeed fulfilled. You then have to check the other conditions a) and b). I let you do it.

mathcounterexamples.net
  • 70,018
  • 1
    I suppose one also wants to be sure that $\max$ deserves its name, i.e., something like $\max{x,y}\ge x$, $\max{x,y}\ge y$, and $\max{x,y}=x\lor \max{x,y}=y$ (with equality of real numbers, not as sets, see p. 58). – Hagen von Eitzen Jun 26 '18 at 20:36
  • @HagenvonEitzen Sure. This has to be part of the things to validate. By the way have you encountered before this construction of the reals? – mathcounterexamples.net Jun 26 '18 at 20:38