Timeline for Can the real numbers be constructed as/from a Hom-object in a topos?
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 15 at 18:03 | comment | added | Mike Shulman | 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$. | |
| Nov 15 at 18:00 | comment | added | Mike Shulman | 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. | |
| Nov 14 at 19:32 | comment | added | Peter LeFanu Lumsdaine | @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. | |
| Nov 14 at 17:50 | comment | added | Mike Shulman | 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}$. | |
| Nov 14 at 17:12 | vote | accept | Steven Stadnicki | ||
| Nov 12 at 16:49 | comment | added | Steven Stadnicki | Thank you! This is a really illuminating answer. | |
| Nov 12 at 7:01 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 4.0 |