Hi !

I'm considering in a general topos $T$ the object $R$ of lower semi-continuous real (one sided lower non-empty Dedekind cuts, as for exemple in http://ncatlab.org/nlab/show/one-sided+real+number ).

I want to know if, even if substraction is not possible, there is (internally) some sort of simplification rules for addition like :

If $x$ is 'bounded' (there exist a rational q such that $x \leqslant q$ ) then $x+a=x+b$ imply $a=b$.

It's seem true to me, but only because of an argument involving a covering of $T$ by a boolean topos, if it's possible I would prefer a completely internal argument, and I can't find it.

[Edited by Andrej Bauer] A lower Dedekind cut is a subset $L \subseteq \mathbb{Q}$ which is

  • rounded: $q \in L \iff \exists r \in L . q < r$
  • inhabited $\exists q \in \mathbb{Q} . q \in L$
  • bounded: $\exists q \in \mathbb{Q} \forall r \in L . r < q$
  • $\begingroup$ Have a look at Davorin Lešnik's PhD thesis, available at fmf.uni-lj.si/storage/19160/PhD_Davorin.pdf. He has an extensive treatment of reals, done constructively and without countable choice. I think he speaks about lower reals as well. $\endgroup$ Sep 25, 2012 at 13:00
  • $\begingroup$ Please write down the definition of a one-sided cut because it is easy to get that wrong in an intuitionistic setting. $\endgroup$ Sep 25, 2012 at 13:01
  • $\begingroup$ Thank you for this reference. I edited my question to include the definition of a cut. $\endgroup$ Sep 25, 2012 at 14:52
  • $\begingroup$ I fixed your definition to make it prettier (but probably equivalent to what you had). $\endgroup$ Sep 25, 2012 at 17:23
  • $\begingroup$ I confirm : this is equivalent. $\endgroup$ Sep 25, 2012 at 22:31

1 Answer 1


Ok I think I finally found an internaly valid proof by my self, so I explain it briefly here in case someone is interested some day :

If $U \in \Omega$ is a subterminal object, you can define the element $1_U \in R$ as :

$q \in 1_U$ when $q < 0 \cup (U \cap q<1)$.

(this correspond to the indicator function of an open set... )

It's easy to show that if $x+1_U \leqslant y + 1_U$ then $x \leqslant y$ :

if $q < x$, then $q < x+1_U$, hence, $\exists u,v$ such that $q=u+v, u < y$ and $v < 0 \cup (v<1 \cap U)$

  • First case : $v<0$ then, $q < u < y$, we have $q < y$.
  • Second case : we have 'U' then $1_U = 1$ so $q+1 < x+1_U$,

    $q+1 < y +1$

    $q < y$

In both case, $q < y$ so $x \leqslant y$.

Now, if $x$ is any bounded positive element, let $N$ be an integer such that $x < N$.

on can define :

$\displaystyle h = \frac{1}{n} \sum_{i=1}^{N.n } 1_{x> (i/n)} $

and one can show that (but it's a little longer) : $h \leqslant x \leqslant h+\frac{1}{n}$.

It's now easy to conclude if $x$ is positive and bounded and $a + x \leqslant x + b$ then if $q < a$, take $q'$ another rational such that $q < q' < a$, let $n$ an integer such that $q'-q < \frac{1}{n}$. and let $h$ be as above :

$ a + h \leqslant a +x \leqslant b+x \leqslant b + h + 1/n $

but by a simple recurence, h can be simplified so :

$ a \leqslant b+1/n $

so $q' < b+1/n$, and finaly $q < q'-1/n < b $

If $x$ is not positive, just take some $q < x$, and $x-q$ will be positive

  • $\begingroup$ I do not understand the definition of $1_U$. What does it mean to take the union of $q < 1$ and $U \cap q < 1$? What does it mean to take the intersection of $U$ and $q < 1$? Are you thinking of $U$ as a truth value, and then $\cup$ and $\cap$ are disjunction and conjunction? Ah, that must be it. So your $1_U$ is $0$ if $U$ is false and $1$ if $U$ is true (but of course that is not a definition). $\endgroup$ Sep 27, 2012 at 12:33
  • $\begingroup$ exactly, I'm thinking of U, q<0 and q<1 as truth value. and $1_U$ is the indicator function. Maybe I should edit to replace $\cup$ by $\vee$ and $\cap$ bu $\wedge$. $\endgroup$ Sep 27, 2012 at 12:41
  • $\begingroup$ I would rewrite your proof a bit. Might do. $\endgroup$ Sep 27, 2012 at 17:16
  • 1
    $\begingroup$ This is great; thanks Simon. I expect a rewrite of your proof (attributed to you) to show up in a paper authored by myself and Tobias Fritz. $\endgroup$ May 15, 2020 at 17:24
  • 1
    $\begingroup$ You're welcome ! In the end I never used it, some I'm happy it is of use to someone ! I still feel the proof should be simpler though, but I never found anything better. $\endgroup$ May 15, 2020 at 18:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.