6
$\begingroup$

I've been reading through Greenblatt's Topoi and while I'm still definitely over my head I'm starting to get a feel for some of the concepts at play there. I see the definitions of $\mathbb{R}_c$ and $\mathbb{R}_d$ in a topos and they somewhat make sense to me, but there's another definition that seems 'natural' that I'm surprised not to find.

Specifically, it seems as though we could define the reals as the (Hom-)set of order-preserving maps $r:\mathbb{Q}\to\Omega$, or more narrowly the subobject here which consists of all such maps such that $r^{-1}(\bot)$ and $r^{-1}(\top)$ are both inhabited. Then, for instance, given reals $f_r():\mathbb{Q}\mapsto\Omega$ and $f_s():\mathbb{Q}\mapsto\Omega$ we can define $f_{r+s}()$ by $f_{r+s}(t)=\bigvee_{p+q=t}\left(f_r(p)\wedge f_s(q)\right)$ (where of course $p, q, t\in\mathbb{Q}$). Given that I haven't seen anything like this I'm presuming that there are conceptual issues with it; I would guess that constructibility is a problem but again I'm very close to drowning in these waters so my knowledge is a bit weak here. Has this definition of reals been looked at at all, and what are the problems with it?

Improve this question
$\endgroup$
2
  • 7
    $\begingroup$ It seems to me that your proposed reals won't satisfy statements like $\forall x\,(x>0\lor x<1)$. So they'd behave very differently from what constructivists (of any sort) usually expect of reals. It also seems to me that, if you modify your proposal to avoid this point, you'll get something very similar to (one-sided) Dedekind reals. $\endgroup$
    – Andreas Blass
    Commented Nov 11 at 20:16
  • 2
    $\begingroup$ I took the liberty of changing the notation in the question to avoid confusion with the numbers 0 and 1, I hope you don't mind. (doubly so, given Andreas' comments) $\endgroup$
    – David Roberts ♦
    Commented Nov 12 at 0:24

2 Answers 2

Reset to default
7
$\begingroup$

Phrased in more everyday language (less diagrammatic), your suggestion amounts to defining reals as proper up-closed subsets of $\newcommand{\Q}{\mathbb{Q}}\newcommand{\R}{\mathbb{R}}\Q$. (Writing the definition of “up-closed” as “if $p \leq q$, then $p \in X \Rightarrow q \in X$”, it’s clear that a subset is up-closed precisely if its characteristic function $\Q \to \Omega$ is order-preserving.) Call this set $\newcommand{\Pup}{\mathcal{P}_\mathrm{pup}}\Pup(\Q)$.

Even in classical set theory, this isn’t a natural construction of the reals: the natural map $\inf : \Pup(\Q) \to \R$ is surjective but not injective, since any rational $r$ will have two preimages, $\Q_{\geq r}$ and $\Q_{>r}$. Or to avoid reference to any other notion of $\R$, we can note that $(\Pup(\Q),\supseteq)$ doesn’t have the order-theoretic properties we expect of the reals: it’s not dense, since it has nothing between $\Q_{\geq r}$ and $\Q_{>r}$.

Classical definitions of (upper) Dedekind cuts remedy this exactly by adding a “left-openness” condition, to exclude cuts of the form $\Q_{\geq r}$. In constructive logic (and hence when working internally to a topos) this turns out to still be a bit deficient, as Simon Henry’s answer notes, and so standard constructive definitions of the Dedekind reals use two-sided cuts, i.e. pairs of subsets $(X_l,X_r)$ with axioms ensuring they’re of the form $(\Q_{<x},\Q_{>x})$.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Thank you! This is a really illuminating answer. $\endgroup$
    – Steven Stadnicki
    Commented Nov 12 at 16:49
  • 1
    $\begingroup$ Though less common, it's also possible, and yields an equivalent result, to instead add a "left-closedness" condition to exclude cuts of the form $\mathbb{Q}_{>r}$. $\endgroup$
    – Mike Shulman
    Commented Nov 14 at 17:50
  • $\begingroup$ @MikeShulman: Interesting; I don’t remember ever seeing that! Can you remember any particular sources that use it, and do you know if it has any advantages? On first it seems a little awkward in several ways — e.g. it looks like addition/multiplication need to be slightly more complicated than in the “open cuts” approach, to add the closed point in case the result is rational. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Nov 14 at 19:32
  • 1
    $\begingroup$ I don't remember where I learned it, and right now I'm failing to find any references. But I remember when I learned it: in order to prove Theorem 9.6 of Affine logic for constructive mathematics, since what arises naturally from the antithesis interpretation is a two-sided cut where one side is open and the other closed. I don't know of any other use for it; as you say, open cuts do seem a bit easier. $\endgroup$
    – Mike Shulman
    Commented Nov 15 at 18:00
  • 1
    $\begingroup$ Also worth noting perhaps is that in Constructivism in Mathematics, Troelstra and van Dalen give a strong notion of one-sided cut that they claim is equivalent to the two-sided version. In addition to boundedness, openness, and locatedness, they add "strong monotonicity": the down-set version is if $p<q$ in $\mathbb{Q}$ and $\neg\neg(q\in X)$, then $p\in X$. $\endgroup$
    – Mike Shulman
    Commented Nov 15 at 18:03
7
$\begingroup$

You can always rewrite a subobject $V \subseteq \mathbb{Q}$ as a function $\mathbb{Q} \to \Omega$, but you'll need to includes all the axiom that are in the definition.

Even if you only look at defining upper Dedekind cut the definition you are proposing is missing the fact that if $x \in V$ then there exists an $x' <x$ such that $x' \in V$.

And upper Dedekind only get you so far, for example you can't define division, substraction, or even unrestricted multiplication with one sidded cut: The more interesting notion of real number (like the Dedekind/continus, or MacNeille) require a pair of such functions for their definition one encodage $x<q$ and one for $q<x$.

Improve this answer
$\endgroup$
5
  • $\begingroup$ I would think that negation could be defined as $f_{-r}(q) = \neg f_r(-q)$, and then subtraction by the formula above. And I'm not sure that my definition needs the fact that $V$ has no minimum; if there is a minimum element $q$ with $f_r(q)=\true$ then we just have $r=q$ (and this does mean there are two functions corresponding to every rational number, but that seems straightforwardly handleable). $\endgroup$
    – Steven Stadnicki
    Commented Nov 12 at 6:56
  • $\begingroup$ Absolutely, that issue is “straightforwardly handleable” — but the most straightforward way to handle it is exactly by adding the extra axiom for Dedekind cuts, as this answer suggests. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Nov 12 at 7:23
  • $\begingroup$ @StevenStadnicki you can define anything you want however you want, but you won't be able to prove any of the expected properties. For example defining $-x$ this way, you don't have $x - x =0$, unless your topos is boolean. While using two sidded cut you get an honest rings. The condition I put in my answer correspodns to the fact that if two real $x$ and $y$ are such that $x <y$, then there exists a real (even a rational) $z$ such that $x <z<y$. So you won't get that either with your definition. $\endgroup$
    – Simon Henry
    Commented Nov 12 at 14:31
  • 1
    $\begingroup$ In fact the Dedekind real are exactly the one sided Dedekind cut $x$ such that there is another one sided cut $y$ satisfying $x+y = 0$. $\endgroup$
    – Simon Henry
    Commented Nov 12 at 15:56
  • $\begingroup$ These make sense to me. Thank you! $\endgroup$
    – Steven Stadnicki
    Commented Nov 12 at 16:48

You must log in to answer this question.

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