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.

]]>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'$.

]]>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.

]]>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.

]]>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.

]]>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'$.

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?

]]>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).

]]>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.

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.

]]>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 also added uniqueness to the properties. (I still need to write in proofs of these properties!)

]]>Okay, thanks very much for the clarification.

]]>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.

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?

]]>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.

]]>Okay, that makes sense – thanks.

]]>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.

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?

]]>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.)

]]>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.

]]>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.

]]>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 field” in the M-B language. It is this that we can prove is unique; and we can prove that the construction from ML-M satisfies it.

Because that would be very interesting, and something I’ve not heard claimed elsewhere. Comment 11 was to sound warnings to the unwary (not meaning you).

]]>Also, *we* have some material on this at field.