Maximum of real numbers

674 Views Asked by At

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.

2

There are 2 best solutions below

2
On

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.

0
On

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$.