nForum - Discussion Feed (Internal Dedekind reals) 2022-08-17T03:52:02-04:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher TobyBartels comments on "Internal Dedekind reals" (25494) https://nforum.ncatlab.org/discussion/3002/?Focus=25494#Comment_25494 2011-08-27T06:25:05-04:00 2022-08-17T03:52:01-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Neat! I was a little worried that my external proof might be bad, since I didn’t say anything about regular epimorphisms, but I think that it’s all right; I proved what I needed to about ...

Neat! I was a little worried that my external proof might be bad, since I didn’t say anything about regular epimorphisms, but I think that it’s all right; I proved what I needed to about $x \lt x'$ and $x' \lt x$, then drew the proper conclusion from this, without going into the details.

Your version is actually simpler than mine when dealing with $L$ and $U$ as parametrised subobjects. I noticed that the generalised element $a$ of $\Gamma$ in my proof could just be the identity morphism, but it seemed more natural to take an arbitrary element as the definition suggested. If that part had been written in the stack semantics all along, then I might have done it differently.

]]>
Mike Shulman comments on "Internal Dedekind reals" (25489) https://nforum.ncatlab.org/discussion/3002/?Focus=25489#Comment_25489 2011-08-27T04:19:23-04:00 2022-08-17T03:52:01-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Here’s the direct translation of your naive proof into stack semantics. Suppose that x,x&prime;&colon;Rx, x'\colon R both satisfy the required properties, and suppose that ...

Here’s the direct translation of your naive proof into stack semantics.

Suppose that $x, x'\colon R$ both satisfy the required properties, and suppose that $x \# x'$.

Suppose that $x, x'\colon \Gamma \to R$ both satisfy the required properties. Suppose additionally that $(x,x')\colon \Gamma \to R\times R$ factors through $[\#]$.

By the strong connectedness of $\lt$, $x \lt x'$ or $x' \lt x$.

By the strong connectedness of $\lt$, there exists a (regular) epimorphism $[p,q]\colon U+V \to \Gamma$ such that $(x,x')p$ factors through $[\lt]$ and $(x',x)q$ factors through $[\lt]$.

Now suppose that $x \lt x'$. It follows that $x$ belongs to $L$, so $x \lt x$.

Since $(x p, x' p)$ factors through $[\lt]$, by assumption on $x'$, we have that $(p,x)$ factors through $L$.

By the strong irreflexivity of $\lt$, $x \# x$; by the irreflexivity of $\#$, we have a contradiction.

This implies that $(x p, x p)$ factors through $[\lt]$, hence also through $[\#]$. But $(x p, x p)$ also factors through $[=]$ (the diagonal of $R$), and irreflexivity of $\#$ means that $[\#]\cap [=] = 0$, the initial object. Therefore, since initial objects are strict, $U$ is also initial.

Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also false.

Similarly, we conclude that $V$ is initial.

Therefore, $x \# x'$ is false.

Since $\Gamma$ is regular epimorphic image of $0+0 = 0$ an initial object, it is also initial, under the hypothesis that $(x,x')\colon \Gamma \to R\times R$ factors through $[\#]$. By definition, this means that without that hypothesis (i.e., given only $x, x'\colon \Gamma \to R$ both satisfying the required properties), we have that $(x,x')$ factors through $\neg [\#]$.

By the tightness of $\#$, $x = x'$.

By the tightness of $\#$, it follows that $(x,x')$ factors through $[=]$, which is to say $x=x'$.

]]>
Zhen Lin comments on "Internal Dedekind reals" (25455) https://nforum.ncatlab.org/discussion/3002/?Focus=25455#Comment_25455 2011-08-26T10:25:47-04:00 2022-08-17T03:52:01-04:00 Zhen Lin https://nforum.ncatlab.org/account/318/ The internal proof is certainly much easier to understand, and I think it illuminates the essence of the proof by hiding irrelevant details. (Do we really need to know about the parametrisation ...

The internal proof is certainly much easier to understand, and I think it illuminates the essence of the proof by hiding irrelevant details. (Do we really need to know about the parametrisation domain $\Gamma$? etc.) On the other hand the given external proof is probably neater than a direct translation of the internal proof into Kripke–Joyal/stack/standard semantics.

]]>
TobyBartels comments on "Internal Dedekind reals" (25443) https://nforum.ncatlab.org/discussion/3002/?Focus=25443#Comment_25443 2011-08-25T21:25:01-04:00 2022-08-17T03:52:01-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Thanks, I’m glad that it makes sense. (And I encourage Zhen Lin and Mike, as well as anybody else, to also reply.) You’ll notice the difference in length. This is a short proof, compared to ...

Thanks, I’m glad that it makes sense. (And I encourage Zhen Lin and Mike, as well as anybody else, to also reply.)

You’ll notice the difference in length. This is a short proof, compared to some of the others, and my worry is that spelling everything out will be very long.

I wonder if I might put this proof in both ways, then write all of the others in the internal language. (Of course, this wouldn’t preclude other people from writing external versions if they wish.)

By the way, I’m just sort of assuming, before I finish his paper, that Mike’s stack semantics interpret the second proof as the first one. If they don’t, then I’m missing the point.

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25442) https://nforum.ncatlab.org/discussion/3002/?Focus=25442#Comment_25442 2011-08-25T20:37:31-04:00 2022-08-17T03:52:01-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Toby, I think it’s legible. But I also think you could put in both the ’naive’ version and the version as you have it, in separate sections if need be. The point is that there will be some ...

Toby, I think it’s legible. But I also think you could put in both the ’naive’ version and the version as you have it, in separate sections if need be.

The point is that there will be some readers who prefer the naive version (together with the highly anti-naive instruction to interpret it in the stack semantics), but others will probably find that too cavalier. Those other readers may prefer the more formal version, but the first set of readers may find it harder to read.

There is plenty of room in the nLab to write in such a way to catch as many readers as possible. I personally tend to feel more comforted by having lots of detail written out.

]]>
TobyBartels comments on "Internal Dedekind reals" (25441) https://nforum.ncatlab.org/discussion/3002/?Focus=25441#Comment_25441 2011-08-25T19:56:38-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Here’s the proof as I wrote it: Suppose that x,x&prime;&colon;&Gamma;&rightarrow;Rx, x'\colon \Gamma \to R both satisfy the required properties, and consider x#x&prime;x \# ...

Here’s the proof as I wrote it:

Suppose that $x, x'\colon \Gamma \to R$ both satisfy the required properties, and consider $x \# x'$, which is a subobject of $\Gamma$. By the strong connectedness of $\lt$, $x \# x'$ is contained in (factors through) $x \lt x' \vee x' \lt x$, which is the union of $x \lt x'$ and $x' \lt x$.

Now consider $x \lt x'$, and let $a$ be a generalised element of $\Gamma$. If $a$ belongs to (factors through) $x \lt x'$, or equivalently $(x(a), x'(a))$ belongs to $\lt$, it follows that $(a,x(a))$ belongs to $L$. Thus, $(x(a), x(a))$ also belongs to $\lt$, or equivalently $a$ belongs to $x \lt x$. By the strong irreflexivity of $\lt$, this is contained in $x \# x$; by the irreflexivity of $\#$, this is contained in $\bot$ (as a subobject of $\Gamma$). Since every $a$ that belongs to $x \lt x'$ belongs to $\bot$, $x \lt x'$ is contained in (and so equals as a subobject) $\bot$.

Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also $\bot$. Therefore, $x \# x'$ is $\bot$. By the tightness of $\#$, $x = x'$.

Here’s the same proof in naïve language:

Suppose that $x, x'\colon R$ both satisfy the required properties, and suppose that $x \# x'$. By the strong connectedness of $\lt$, $x \lt x'$ or $x' \lt x$.

Now suppose that $x \lt x'$. It follows that $x$ belongs to $L$, so $x \lt x$. By the strong irreflexivity of $\lt$, $x \# x$; by the irreflexivity of $\#$, we have a contradiction.

Similarly (either by swapping $x$ with $x'$ or by using $U$ instead of $L$), $x' \lt x$ is also false. Therefore, $x \# x'$ is false. By the tightness of $\#$, $x = x'$.

]]>
TobyBartels comments on "Internal Dedekind reals" (25440) https://nforum.ncatlab.org/discussion/3002/?Focus=25440#Comment_25440 2011-08-25T19:47:18-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ The other day, I put in a proof of the uniqueness of the point determined by a Dedekind cut. Is it legible? Would it be better to simply write a proof in naïve language and instruct the reader to ...

The other day, I put in a proof of the uniqueness of the point determined by a Dedekind cut. Is it legible? Would it be better to simply write a proof in naïve language and instruct the reader to interpret it in the stack semantics?

]]>
Zhen Lin comments on "Internal Dedekind reals" (25302) https://nforum.ncatlab.org/discussion/3002/?Focus=25302#Comment_25302 2011-08-20T09:13:06-04:00 2022-08-17T03:52:02-04:00 Zhen Lin https://nforum.ncatlab.org/account/318/ Toby: Ah, that's what I thought a parametrised subobject would be. Thanks for clarifying. Mike: That looks quite nice! I haven't had time to digest the whole of the paper yet, but it seems like ...

Toby: Ah, that's what I thought a parametrised subobject would be. Thanks for clarifying.

Mike: That looks quite nice! I haven't had time to digest the whole of the paper yet, but it seems like definition 7.2 would make a good starting point for an article on stack semantics (or, for that matter, Kripke–Joyal semantics, appropriately modified).

]]>
Mike Shulman comments on "Internal Dedekind reals" (25295) https://nforum.ncatlab.org/discussion/3002/?Focus=25295#Comment_25295 2011-08-20T02:27:06-04:00 2022-08-17T03:52:02-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ And if you prefer not to have to think about generalized elements and parametrized subobjects all the time, then the stack semantics is a way to package them up “once and for all”, so that you ...

And if you prefer not to have to think about generalized elements and parametrized subobjects all the time, then the stack semantics is a way to package them up “once and for all”, so that you can just say things like

An ordered field object R is Dedekind-complete if it satisfies the sentence “for all Dedekind cuts (L,U) in R, there exists an element $x\in R$ such that $L = \{ b\in R | b\lt x\}$ and $U = \{ b\in R | x\lt b\}$” in the stack semantics.

]]>
TobyBartels comments on "Internal Dedekind reals" (25275) https://nforum.ncatlab.org/discussion/3002/?Focus=25275#Comment_25275 2011-08-19T04:47:00-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Regarding parametrised subobjects (which Zhen Lin called “still a mystery”): notice that in the construction of an RNO in a topos, LL (half of Dedekind cut) was given as a generalised element of ...

Regarding parametrised subobjects (which Zhen Lin called “still a mystery”): notice that in the construction of an RNO in a topos, $L$ (half of Dedekind cut) was given as a generalised element of $\mathcal{P}\mathbb{Q}$, that is a morphism from some object $\Gamma$ to $\mathcal{P}\mathbb{Q}$. But morphisms from $\Gamma$ to $\mathcal{P}\mathbb{Q}$ are in natural bijection with subobjects of $\Gamma \times \mathbb{Q}$. And that is a parametrised subobject of $\mathbb{Q}$, which is what $L$ is in the general definition (except using $R$ in place of $\mathbb{Q}$, since I’m giving the condition for $R$ to be Dedekind-complete rather than constructing the Dedekind completion of $\mathbb{Q}$).

So, if you can do generalised elements, then you can do parametrised subobjects.

]]>
TobyBartels comments on "Internal Dedekind reals" (25274) https://nforum.ncatlab.org/discussion/3002/?Focus=25274#Comment_25274 2011-08-19T01:47:32-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I now have the complete definition of an RNO in an arbitrary Heyting category. Also, the properties are stated as precise theorems (but still requiring proofs).

I now have the complete definition of an RNO in an arbitrary Heyting category. Also, the properties are stated as precise theorems (but still requiring proofs).

]]>
TobyBartels comments on "Internal Dedekind reals" (25272) https://nforum.ncatlab.org/discussion/3002/?Focus=25272#Comment_25272 2011-08-19T00:23:37-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I also added uniqueness to the properties. (I still need to write in proofs of these properties!)

I also added uniqueness to the properties. (I still need to write in proofs of these properties!)

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25271) https://nforum.ncatlab.org/discussion/3002/?Focus=25271#Comment_25271 2011-08-19T00:21:49-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Okay, thanks very much for the clarification.

Okay, thanks very much for the clarification.

]]>
TobyBartels comments on "Internal Dedekind reals" (25270) https://nforum.ncatlab.org/discussion/3002/?Focus=25270#Comment_25270 2011-08-19T00:19:06-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ No, that’s not what I’m doing. The Cauchy construction goes through in any &Pi;\Pi-pretopos with an NNO (and every topos is a &Pi;\Pi-pretopos). However, only if the ...

No, that’s not what I’m doing.

The Cauchy construction goes through in any $\Pi$-pretopos with an NNO (and every topos is a $\Pi$-pretopos). However, only if the $\Pi$-pretopos satsifies $WCC$ will the Cauchy construction give an RNO. (Most toposes don’t satisfy $WCC$, although Boolean toposes do, and so does the effective topos.) This is the second construction.

On the other hand, if the $\Pi$-pretopos satisfies subset collection (which every topos does), then it is also possible to modify the Cauchy construction in such a way that the modified construction does give an RNO. This is the third construction.

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25269) https://nforum.ncatlab.org/discussion/3002/?Focus=25269#Comment_25269 2011-08-19T00:00:50-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ I would love to see details! I have to say: this look awfully tricky to me. You appear to be using the Cauchy definition in the context of a &Pi;\Pi-pretopos, and asserting that this specializes ...

I would love to see details!

I have to say: this look awfully tricky to me. You appear to be using the Cauchy definition in the context of a $\Pi$-pretopos, and asserting that this specializes to the Dedekind reals in the case of a topos?

]]>
TobyBartels comments on "Internal Dedekind reals" (25261) https://nforum.ncatlab.org/discussion/3002/?Focus=25261#Comment_25261 2011-08-18T23:34:20-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I have put in the definition of RNO in an arbitrary Heyting pretopos, but I want to add details. I’ve also put in an outline of the rest of what I want to write.

I have put in the definition of RNO in an arbitrary Heyting pretopos, but I want to add details. I’ve also put in an outline of the rest of what I want to write.

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25116) https://nforum.ncatlab.org/discussion/3002/?Focus=25116#Comment_25116 2011-08-13T01:18:32-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Okay, that makes sense – thanks.

Okay, that makes sense – thanks.

]]>
TobyBartels comments on "Internal Dedekind reals" (25115) https://nforum.ncatlab.org/discussion/3002/?Focus=25115#Comment_25115 2011-08-13T00:24:40-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ See #8 again; in the general context, I’d only define it and prove uniqueness. To prove existence (to construct the RNO), I need a stronger context (not necessarily a topos, but with at least some ...

See #8 again; in the general context, I’d only define it and prove uniqueness. To prove existence (to construct the RNO), I need a stronger context (not necessarily a topos, but with at least some second-order constructions).

A two-sided Dedekind cut $L,U$ is located if, whenever $a \lt b$ as rational numbers, $a \in L$ or $b \in U$ (property (7) at Dedekind cut). This is actually only the beginning of a massive generalisation (perhaps one day at located subspace), all of which is classically trivial. If you replace (7) with something weaker, then you get a stronger notion of completeness.

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25114) https://nforum.ncatlab.org/discussion/3002/?Focus=25114#Comment_25114 2011-08-12T20:21:59-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Thanks, Toby. But I’m sorry, I don’t know what ’located’ means here. I’m also confused by the fact that you are working in the context of a Heyting pretopos. This gives a context for ...

Thanks, Toby. But I’m sorry, I don’t know what ’located’ means here.

I’m also confused by the fact that you are working in the context of a Heyting pretopos. This gives a context for internalizing intuitionistic first-order logic in a category (right?), but I always think of the construction of the reals as being a second-order construction. At the risk of asking a stupid question: how will you construct an object of cuts in your context? Are you assuming some higher-order constructions?

]]>
TobyBartels comments on "Internal Dedekind reals" (25112) https://nforum.ncatlab.org/discussion/3002/?Focus=25112#Comment_25112 2011-08-12T18:32:54-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I can’t get at my copy of the Elephant right now, so I don’t know what’s in D.4.7.11. But for “completeness” I intend to use completeness under located Dedekind cuts, which is sufficient ...

I can’t get at my copy of the Elephant right now, so I don’t know what’s in D.4.7.11. But for “completeness” I intend to use completeness under located Dedekind cuts, which is sufficient for uniqueness of the RNO and for existence in each of the three cases listed in #6. As for whether this RNO additionally satisfies stronger notions of “completeness” (which is what I’m guessing D.4.7.11 is about), that would only happen in certain categories. (And my intended general context is a Heyting pretopos, since that’s the most general situation that I care about, and I actually don’t know how to make it work in a more general context.)

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25111) https://nforum.ncatlab.org/discussion/3002/?Focus=25111#Comment_25111 2011-08-12T16:21:35-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Okay, I’ll be interested to see how you treat completeness (I take it you are working in the context of an arbitrary topos). In particular, why the restrictions on the topos implied by Elephant’s ...

Okay, I’ll be interested to see how you treat completeness (I take it you are working in the context of an arbitrary topos). In particular, why the restrictions on the topos implied by Elephant’s theorem D.4.7.11 do not impinge on your treatment.

]]>
TobyBartels comments on "Internal Dedekind reals" (25109) https://nforum.ncatlab.org/discussion/3002/?Focus=25109#Comment_25109 2011-08-12T16:12:06-04:00 2022-08-17T03:52:02-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Yes, except for the fairness of the phrase “universal property”, which is probably not really appropriate. (There are approaches to constructing &Ropf;\mathbb{R} or [0,1][0,1] as an ordered ...

Yes, except for the fairness of the phrase “universal property”, which is probably not really appropriate. (There are approaches to constructing $\mathbb{R}$ or $[0,1]$ as an ordered set that lay better claim to this term, but that’s not what I’m talking about, and I don’t think that they give the same result as the located Dedekind RNO in an arbitrary topos.) I just need a block of time in front of a decent keyboard to write it out.

]]>
Todd_Trimble comments on "Internal Dedekind reals" (25108) https://nforum.ncatlab.org/discussion/3002/?Focus=25108#Comment_25108 2011-08-12T15:27:55-04:00 2022-08-17T03:52:02-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Okay, good! So you feel pretty confident about this claim? Yes, it is basically a universal property of RNOs that I want to put in, a complicated one, which essentially says “complete ordered ...