Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeJan 27th 2014
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexAdded to _[[Dedekind cut]]_ a short remark on the $\neg\neg$-stability of membership in the lower resp. the upper set of a Dedekind cut.

   Added to Dedekind cut a short remark on the $\neg\neg$-stability of membership in the lower resp. the upper set of a Dedekind cut.

2. • CommentRowNumber2.
   • CommentAuthorTobyBartels
   • CommentTimeJan 27th 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexInteresting! I didn\'t quite follow the last bit of your argument, so I rephrased it. (I also regularized the notation of $R$ vs $U$ and finagled a link to [[stable property]].)

   Interesting! I didn't quite follow the last bit of your argument, so I rephrased it. (I also regularized the notation of $R$ vs $U$ and finagled a link to stable property.)

3. • CommentRowNumber3.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeJan 27th 2014
   • (edited Jan 27th 2014)
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexThanks for catching the typo and streamlining the argument! (For the record, my reasoning was as follows: Since $b \in U$, we have $\neg\neg(b \in U)$. Since $\neg\neg(b \in L)$ and $\neg\neg$ distributes over $\wedge$, we have $\neg\neg(b \in L \wedge b \in R)$. Since $b \in L \wedge b \in R \Rightarrow \bot$ and $\neg\neg$ is monotone, we have $\neg\neg\bot$, so $\bot$.) The almost-$\neg\neg$-stability can be helpful when proving the equivalence of Dedekind cuts with multi-valued Cauchy "sequences" (i.e. certain maps $\mathbb{Q}^+ \to P(\mathbb{Q})$). Depending on one's line of thought, of course, one can otherwise get stuck when trying to show that _equivalent_ multi-valued Cauchy sequences define the _same_ Dedekind cut.

   Thanks for catching the typo and streamlining the argument! (For the record, my reasoning was as follows: Since $b \in U$, we have $\neg\neg(b \in U)$. Since $\neg\neg(b \in L)$ and $\neg\neg$ distributes over $\wedge$, we have $\neg\neg(b \in L \wedge b \in R)$. Since $b \in L \wedge b \in R \Rightarrow \bot$ and $\neg\neg$ is monotone, we have $\neg\neg\bot$, so $\bot$.)

   The almost-$\neg\neg$-stability can be helpful when proving the equivalence of Dedekind cuts with multi-valued Cauchy “sequences” (i.e. certain maps $\mathbb{Q}^+ \to P(\mathbb{Q})$). Depending on one’s line of thought, of course, one can otherwise get stuck when trying to show that equivalent multi-valued Cauchy sequences define the same Dedekind cut.

4. • CommentRowNumber4.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeSep 25th 2014
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexAdded a short remark that equality of Dedekind cuts is $\neg\neg$-stable.

   Added a short remark that equality of Dedekind cuts is $\neg\neg$-stable.

5. • CommentRowNumber5.
   • CommentAuthorDavidRoberts
   • CommentTimeJul 17th 2018
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAdded Project Gutenberg link for Beman's English translation of _Continuity and irrational numbers_ <a href="https://ncatlab.org/nlab/revision/diff/Dedekind+cut/20">diff</a>, <a href="https://ncatlab.org/nlab/revision/Dedekind+cut/20">v20</a>, <a href="https://ncatlab.org/nlab/show/Dedekind+cut">current</a>

   Added Project Gutenberg link for Beman’s English translation of Continuity and irrational numbers

   diff, v20, current

6. • CommentRowNumber6.
   • CommentAuthorGuest
   • CommentTimeApr 14th 2022
   • PermaLink
   Author: Guest
   Format: MarkdownItexWhen editing is available again on the nLab, I think it would be a good idea to talk about the definition of Dedekind cuts in terms of $\sigma$-frames $\Sigma$ as the set of open truth values, such as [[Sierpinski space]] $\mathbb{S}$, and pairs of open subspaces $(L, U):(\mathbb{Q} \to \Sigma) \times (\mathbb{Q} \to \Sigma)$, as is common in predicative constructive mathematics and [[formal topology]].

   When editing is available again on the nLab, I think it would be a good idea to talk about the definition of Dedekind cuts in terms of $\sigma$-frames $\Sigma$ as the set of open truth values, such as Sierpinski space $\mathbb{S}$, and pairs of open subspaces $(L, U):(\mathbb{Q} \to \Sigma) \times (\mathbb{Q} \to \Sigma)$, as is common in predicative constructive mathematics and formal topology.

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeFeb 21st 2023
   • PermaLink
   Author: Urs
   Format: MarkdownItexpolished up the existing reference items and added these pointers: * [[Andrej Bauer]], [[Paul Taylor]], *The Dedekind reals in abstract Stone duality*, Mathematical Structures in Computer Science **19** 4 (2009) 757-838 &lbrack;[doi:10.1017/S0960129509007695](https://doi.org/10.1017/S0960129509007695)&rbrack; * [[Andrej Bauer]], *Efficient Computation with Dedekind Reals*, talk at *[Computability and complexity in analysis 2008](https://math.andrej.com/2008/08/24/efficient-computation-with-dedekind-reals/)* and at *[Mathematics, Algorithms and Proofs 2008](http://cdsagenda5.ictp.trieste.it/full_display.php?smr=0&ida=a07167)* (2008) &lbrack;[web](https://math.andrej.com/2008/08/24/efficient-computation-with-dedekind-reals/), slides: [pdf](https://math.andrej.com/wp-content/uploads/2008/08/slides-map2008.pdf), extended abstract: [pdf](https://math.andrej.com/wp-content/uploads/2008/08/abstract-cca2008.pdf)&rbrack; <a href="https://ncatlab.org/nlab/revision/diff/Dedekind+cut/33">diff</a>, <a href="https://ncatlab.org/nlab/revision/Dedekind+cut/33">v33</a>, <a href="https://ncatlab.org/nlab/show/Dedekind+cut">current</a>

   polished up the existing reference items

   and added these pointers:

   • Andrej Bauer, Paul Taylor, The Dedekind reals in abstract Stone duality, Mathematical Structures in Computer Science 19 4 (2009) 757-838 [doi:10.1017/S0960129509007695]

   • Andrej Bauer, Efficient Computation with Dedekind Reals, talk at Computability and complexity in analysis 2008 and at Mathematics, Algorithms and Proofs 2008 (2008) [web, slides: pdf, extended abstract: pdf]

   diff, v33, current