6
$\begingroup$

Statement:

Let $$X=$$ $$\{(a,b) \in \mathbb{R} \setminus \{0\} \times \mathbb{R}\setminus \{0\}:a<b\}$$ There exists a function $f:X \rightarrow \mathbb{R} \setminus \{0\}$ 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 proved this statement constructively without using the axiom of countable choice, but for doing that, I assumed real numbers are regular sequences of rational numbers (according to Bishop).

The idea of the proof is that you construct a rational number $q$ such that $|q-b| < \frac{3}{4}|a-b|$ and $|q-a| < \frac{3}{4}|a-b|$. If $q=0$ then put $f(a,b)=\frac{\frac{a+b}{2}+b}{2}$ and if $\neg(q=0)$ then put $f(a,b)=q$.

Now I wonder how can we prove this statement by considering real numbers as Dedekind cuts of rational numbers? i.e if we consider real numbers as Dedekind cuts, can we prove this statement constructively without using the axiom of countable choice?

The proof that I mentioned doesn't go well if reals are Dedekind reals, because we cannot easily construct the desired rational number, if we restrict ourselves to not use the axiom of countable choice.

Can anyone help me with this? Thank you.

$\endgroup$
8
  • 3
    $\begingroup$ Doesn't it work to just explicitly define the function by $f(a,b)=\frac12 a+\frac12 b$ which works everywhere except the line $b=a$, and define it by $f(a,b)=\frac23 a + \frac13 b$ or something on that line? $\endgroup$
    – Zoe Allen
    Commented Apr 23 at 4:16
  • 3
    $\begingroup$ Just a question, by $\mathbb{R}\setminus\{0\}$, do you mean the set of $x$ with $x \# 0$ or merely $x \neq 0$? $\endgroup$
    – S.C.
    Commented Apr 23 at 7:24
  • 1
    $\begingroup$ @Mohammadtahmasbizade what do you mean by "cannot decide constructively"? And why on the contrary "constructing a rational number $q$ such that (...)" is constructive? I don't see how the axiom of (countable) choice is related to models of real numbers to be honest. These all satisfy axioms of real numbers regardless of the axiom of (countable) choice. In particular equality of real numbers is independent of axiom of (countable) choice. Unless by "constructively" you mean something else? $\endgroup$
    – freakish
    Commented Apr 23 at 8:30
  • 4
    $\begingroup$ @freakish, I think the natural interpretation of "constructive" in this post does not have to do with the axiom of choice, but rather with the law of the excluded middle - ie it's about intuitionistic mathematics and the fact that equality of reals is not constructively decidable. (See also the tag description for constructive-mathematics) $\endgroup$
    – Izaak van Dongen
    Commented Apr 23 at 10:51
  • 2
    $\begingroup$ Mohammad, could you say in your post exactly how you define "Dedekind real" constructively, and moreover what constructive system you're working in? This may affect what a useful answer to your post looks like. Or are you interested in what happens with various different definitions and systems? $\endgroup$
    – Izaak van Dongen
    Commented Apr 23 at 11:04

1 Answer 1

Reset to default
3
$\begingroup$

Restrict to $a<0<b$, and let $g:(0,1)\to\mathbb{R}$, $g(z)=f(a,(1-z^{-1})a)/(z^{-1}a)$. Then $g(\tfrac{1}{5})<0$, $g(\tfrac{4}{5})>0$, and for all $z$ we have $\neg(g(z)=0)$.

But there exists a topos in which all endofunctions of the Dedekind reals are continuous and the conventional "strong" version of the intermediate value theorem holds (Bauer and Hanson 2024). In this model the existence of $g$ (and therefore $f$) entails a contradiction. It must be, then, that we are not able to derive the existence of the supposed $f$ within the confines of intuitionistic logic.

$\endgroup$
1
  • $\begingroup$ You answered my question! That was a good answer. Thank you. I wonder in the model you mentioned, is it the case that all endofunctions of R^f are continuous and the conventional strong version of intermediate value theorem holds as well? By R^f, I mean the set of all equivalence classes of fundamental sequences. $\endgroup$
    – Mohammad tahmasbi zade
    Commented Sep 11 at 3:11

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .