Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.)
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.
Added a short remark that equality of Dedekind cuts is $\neg\neg$-stable.
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.
1 to 6 of 6