# Simplification in Semi-continuous real ?

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$
• 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. Sep 25 '12 at 13:00
• Please write down the definition of a one-sided cut because it is easy to get that wrong in an intuitionistic setting. Sep 25 '12 at 13:01
• Thank you for this reference. I edited my question to include the definition of a cut. Sep 25 '12 at 14:52
• I fixed your definition to make it prettier (but probably equivalent to what you had). Sep 25 '12 at 17:23
• I confirm : this is equivalent. Sep 25 '12 at 22:31

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

• 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). Sep 27 '12 at 12:33
• 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$. Sep 27 '12 at 12:41
• I would rewrite your proof a bit. Might do. Sep 27 '12 at 17:16
• 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. May 15 '20 at 17:24
• 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. May 15 '20 at 18:37