Finding an irrational number between two given irrational numbers constructively

Question

Statement:

Let $$X=\{(a,b) \in \mathbb{R} \setminus \mathbb{Q} \times \mathbb{R} \setminus \mathbb{Q}:a<b\}$$ There exists a function $f:X \rightarrow \mathbb{R} \setminus \mathbb{Q}$ such that for all $(a,b) \in X$, $|f(a,b)-b| \le \frac{3}{4}|a-b|$ and $|f(a,b)-a| \le \frac{3}{4}|a-b|$.

I want to prove this statement constructively, whitout using axiom of countable choice (or any other choice axiom) and also I don't want to use any special definition of real numbers (such as regular sequences of rational numbers, Dedekind cuts, etc). I just want to use the usual order properties of real numbers and other properties that all standard constructive definitions of real numbers admit (for example, Archimedian property, Cauchy completeness property, if $a<b$ then $a+c<b+c$ for all real numbers $a,b$ and $c$, etc).

What I have achieved so far, is that if we prove the following statement (by limitations that I mentioned), we are done:

There is a function which assign to any $i,j \in \mathbb{R} \setminus \mathbb{Q}$, a real number $c \in \mathbb{R} \setminus \mathbb{Q}$ such that both sets $\{i,c,1\}$ and $\{j,c,1\}$ are rational independent.

But I couldn't prove that, and I couldn't go further. Any help would be appreciated. Thanks.

Answer 1

In what follows, we assume that the reals form an ordered field $(\mathbb{R}, <, +, \cdot, \min, \max, 0, 1)$ that properly extends $\mathbb{Q}$ and is Archimedean in the strongly constructive sense that we have

• a fixed element $r \in \mathbb{R} \setminus \mathbb{Q}$, and
• a fixed function $q: \{(a,b) \in \mathbb{R}^2 \mid a < b\} \rightarrow \mathbb{Q}$ satisfying $a < q(a,b) < b$ for all $a,b$ in the domain of $q$.

The usual constructions of Cauchy real numbers in constructive settings, including e.g. the reals of the HoTT book, satisfy these assumptions: but one has to be careful, there might be other, quotient-based constructions which would classically yield the reals, but constructively do not give you an Archimedean property (e.g. because the rationals you could get always depend on the representatives of the equivalence classes). I don't know whether you can prove the theorem by other methods that would avoid appeals to the Archimedean property.

We can construct the desired irrational $x$ in two steps. First, given $a < b \in \mathbb{R} \setminus \mathbb{Q}$, we find two rationals $L < U$ satisfying all of the following:

• $a + \frac{1}{4}(b-a) < L$,
• $L < U$,
• $U < b - \frac{1}{4}(b - a)$.

Then we find an $x \in \mathbb{R} \setminus \mathbb{Q}$ such that $L < x < U$, which satisfies all your the desiderata for the value $f(a,b)$. Finally, we write down a formula for the function $f$.

I. Constructing $L$ and $U$

Use the Archimedean property to define the rational-valued functions $$\ell(a,b) = q(a,q(a,b))$$ $$u(a,b) = q(q(a,b),b)$$ and to conclude that $a < \ell(a,b) < u(a,b) < b$ for any $a < b \in \mathbb{R}$.

Given $a < b$ as in the question, the usual order properties of the reals yield $0 < \frac{1}{2}(b - a) < (b - a)$ and therefore

1. $\frac{1}{2}(b-a) < (b-a)$
2. $\frac{1}{4}(b-a) < (b-a) - \frac{1}{4}(b-a)$
3. $a + \frac{1}{4}(b-a) < b - \frac{1}{4}(b-a)$

all hold. To simplify notation, set $A = a + \frac{1}{4}(b - a)$ and $B = b - \frac{1}{4}(b - a)$. These satisfy $A < B$, so set $L = \ell(A,B)$ and $U = u(A,B)$.

II. Constructing $x$ such that $L < x < U$

Since $\mathbb{R}$ properly extends $\mathbb{Q}$, we have some $r \in \mathbb{R} \setminus \mathbb{Q}$. Note that I establish this constructively for all the usual explicit constructions of the reals in another answer, by showing that $\log_2 3$ is irrational and lies in the interval $[1,2]$: so if you have a specific construction, you can skip a large part of this section by setting $R = \log_2 3 - 1$ instead of constructing the number $R$ below.

By the usual ordered field properties we have $r-1 < r < r+1$, so we can use the Archimedean property to choose rationals $q(r,r+1)$ and $q(r-1,r)$. Since the order on the rationals is decidable, determine if $0 < q(r-1,r)$. If yes, let $|r|$ denote $r$. If not, determine if $q(r,r+1) < 0$, and if so, let $|r|$ denote $-r$. Finally, if neither holds, let $|r| = r + 2$. In any case, $0<|r| \in \mathbb{R}\setminus \mathbb{Q}$ (exercise!).

Using the Archimedean property, have $0 < |r| < q(|r|,|r| + 1)$. Set $R = \frac{|r|}{q(|r|,|r| + 1)}$ and conclude that $0 < R < 1$ and $R \in \mathbb{R} \setminus \mathbb{Q}$ hold.

Set $x = L + R(U - L)$. Clearly, $x \in \mathbb{R} \setminus \mathbb{Q}$, and $R(U - L) < (U - L)$, so $x$ satisfies all the required conditions.

III. A formula for $f$

We can expand the abbreviations used above and write down a nigh-unreadable explicit formula for the function $f$ as follows:

1. $f(a,b) = x$
2. $f(a,b) = L + R(U - L)$
3. $f(a,b) = \ell(A,B) + R(u(A,B) - \ell(A,B))$
4. $f(a,b) = q(A,q(A,B)) + R(q(q(A,B),B) - q(A,q(A,B)))$
5. $f(a,b) = q(a + \frac{1}{4}(b-a),q(a + \frac{1}{4}(b-a),b - \frac{1}{4}(b-a))) + R(q(q(a + \frac{1}{4}(b-a),b - \frac{1}{4}(b-a)),b - \frac{1}{4}(b-a)) - q(a + \frac{1}{4}(b-a),q(a + \frac{1}{4}(b-a),b - \frac{1}{4}(b-a))))$

You could further expand the definition of $R \in \mathbb{R} \setminus \mathbb{Q}$ (or even set $R = \log_2 3 - 1$ as mentioned above), and by filling in a couple of proof obligations, even obtain a function definition in a proof assistant / interactive theorem proving software such as Agda/Rocq.

edit: The Archimedean property

In response to comments, let me sketch why the strategy presented above cannot work for constructive presentations of real numbers which do not admit the strong Archimedean property. This happens e.g. if you present the reals as a quotient under convergence instead of just defining an "equiconvergence" relation, or if you are not satisfied with a mere set-function $q: \mathbb{R} \rightarrow \mathbb{Q}$, but also want $q$ to preserve the equiconvergence relation (i.e. you want $q$ to be a setoid-function).

It's well-known that some presentations $(R, <, +, \cdot, \min, \max, 0, 1)$ of the reals in certain foundations are consistent with (or if the foundation is Brouwerian, even outright prove) the principle that all functions $f: [0,1] \rightarrow [0,1]$ are continuous, where $[0,1]$ denotes the unit interval of $R$.

In such presentations, if you could define a function $f: \{(a,b) \in \mathbb{R}^2 \mid a < b\} \rightarrow \mathbb{Q}$ so that $a < f(a,b) < b$, you could use the fact that $x \mapsto \lceil x \rceil$ is defined on $\mathbb{Q}$ (albeit not on $R$) to create $x \mapsto \frac{1}{\lceil q(x,\max(x+1,1)) \rceil}$, which would constitute a discontinuous map from $[0,1]$ to itself. This would contradict the continuity principle.

Consequently, if there is a positive answer to the question, one which is general enough to work even on such presentations $R$, it necessarily has to make use of the restriction to $R \setminus \mathbb{Q}$. As I mentioned above, I don't know whether you can prove the result by methods that would avoid appeals to the Archimedean property. Keep in mind, though, that none of the answers posted to date (deleted or not) make any use of this property, and hencenone of them work at this level of generality.

Answer 2

There exists a rational number $c\in\left(\frac{a+b}2,b\right)$; this can be found constructively. Then the desired number is $\frac{a+c}2$, which can easily be shown to satisfy the required inequalities.