The Dedekind completion of a linear order $L$ is a new linear order $\widebar{L}$ that contains suprema for all inhabited bounded subsets, and such that a supremum in $L$ is still a supremum in $\widebar{L}$.
While Dedekind completeness was traditionally described in the context of the real numbers, it can be stated for any linear order, although it really works best for dense? and unbounded (without top or bottom) linear orders. Intuitively, a linear order is Dedekind complete if Dedekind cuts don’t give any ‘new’ elements.
Let $S$ be a set equipped with the structure of a dense linear order without top or bottom elements (endpoints).
A cut in $S$ is a pair of subsets $L, U \subset S$ of $S$ that satisfy the following eight properties:
The linearly ordered set $S$ is Dedekind complete if every cut $(L,U)$ is of the form
for some unique $a \in S$.
If $T$ is also an unbounded dense linear order, $S$ is Dedekind complete, and we have a universal arrow $u\colon T \to S$ in the category of linear orders, then $S$ (equipped with $u$) is the Dedekind completion of $T$.
The set of Dedekind cuts of rational numbers –the set of real numbers– is Dedekind complete. In fact, starting with any unbounded dense linearly ordered set $S$, the set of Dedekind cuts is isomorphic to the reals as long as $S$ is a countably infinite set.
The operation of forming the set of Dedekind cuts is idempotent, so the Dedekind completion can be constructed as the set of Dedekind cuts. More precisely, the Dedekind-complete linear orders form a reflective subcategory of the category of dense unbounded linear orders, so that Dedekind completion is a kind of completion in the abstract categorial sense.
A set $F$ with a linear order is Dedekind complete if
For all elements $a \in F$ and $b \in F$, the open interval $(a,b)$ is inhabited.
For all elements $a \in F$, the upper unbounded open interval $(a,\infty)$ is inhabited.
For all elements $a \in F$, the lower unbounded open interval $(-\infty,a)$ is inhabited.
For all elements $a \in F$ and $b \in F$, $a \lt b$ if and only if $(b,\infty)$ is a subinterval of $(a,\infty)$
For all elements $a \in F$ and $b \in F$, $b \lt a$ if and only if $(-\infty,b)$ is a subinterval of $(-\infty,a)$
For all elements $a \in F$ and $b \in F$, if $a \lt b$, then $F$ is a subinterval of the union of $(a, \infty)$ and $(-\infty, b)$
For all elements $a \in F$ and $b \in F$, the intersection of $(a,\infty)$ and $(-\infty,b)$ is a subinterval of the open interval $(a,b)$
In predicative constructive mathematics, subsets are large and therefore are proper classes. Thus, any Dedekind completion of a dense linear order, and in particular the rational numbers, is a proper class. Instead, predicative constructive mathematicians typically use pairs of functions $L, U: \mathbb{Q} to \Sigma$ representing the open subsets of $\mathbb{Q}$ to define predicative cuts, where $\Sigma$ is a small $\sigma$-frame with an embedding $\Sigma \to \mathrm{Prop}_\mathcal{U}$ into the large set of propositions for a universe $\mathcal{U}$. The definitions then become
Given a small $\sigma$-frame $\Sigma$ that embeds into the large set of propositions $\mathrm{Prop}_\mathcal{U}$ for a universe $\mathcal{U}$ and a linearly ordered set $S$, a cut in $S$ is a pair of functions $L, U: S to \Sigma$ that satisfy the following eight properties:
The linearly ordered set $S$ is $\Sigma$-Dedekind complete if for every cut $(L,U)$ there exists a unique element $a \in S$ such that for all elements $x \in S$, $x \lt a$ implies $L(x) = \top$ and $x \gt a$ implies $U(x) = \top$.
Given any linearly ordered set $S$, for any two $\sigma$-frames $\Sigma$ and $\Sigma^{'}$ that embed into $\mathrm{Prop}_\mathcal{U}$ such that $\Sigma \subseteq \Sigma^{'}$, if $A$ is the $\Sigma$-Dedekind completion of $S$ and $B$ is the $\Sigma^{'}$-Dedekind completion of $S$, then $A \subseteq B$.
Any paragraph containing the string ‘duiq’ is original research (although lower duiqs at least are known in domain theory).
One can generalise Dedekind completion from linear orders to quasiorders.
A duiq (dense unbounded inhabited quasiorder) is a quasiordered set $S$ such that, given finite (here always meaning Kuratowski-finite) subsets $F$ and $G$ of $S$ such that $x \lt z$ whenever $x \in F$ and $z \in G$, we have some $y$ in $S$ such that $x \lt y \lt z$ whenever $x \in F$ and $z \in G$.
Note that, for $S$ a linear order, $S$ is a duiq iff $S$ is dense, unbounded, and inhabited, hence the term ‘duiq’. (Using linearity, we may assume that $F$ and $G$ are subsingletons; then two singleton subsets is denseness, one singleton subset and one empty subset is unboundedness, and two empty subsets is inhabitedness.)
Given a duiq $S$, a cut is a pair $(L,U)$ of subsets such that:
We then define Dedekind-complete duiqs and Dedekind completions of duiqs the same as for dense linear orders, using this notion of cut.
A good example of a duiq is the set of rational-valued functions on any set $X$; the Dedekind completion is the set of real-valued functions on $X$.
Sections 4.31–39 of HAF do things in even more generality, but I don't really understand it yet.
At least in classical mathematics, considering only $L$ (for a lower cut) or $U$ (for an upper cut) doesn't really give us anything new for linear orders; we have only the technicality that $\infty \coloneqq (S,\empty)$ or $-\infty \coloneqq (\empty,S)$ is a cut (depending on the side), and we can rule even these out by simply requiring that $L$ have an upper bound or that $U$ have a lower bound.
In constructive mathematics, one-sided cuts are more general; see one-sided real number for a discussion of the case where $S$ is the linear order of rational numbers.
Even in classical mathematics, one-sided cuts do give us something new for quasiorders. Here, we have first more general one-sided notions of duiqs: a lower duiq need only satisfy the condition of a duiq for $G$ a singleton, and an upper duiq need only satisfy the condition for $F$ a singleton. Then the lower Dedekind completion of a lower duiq is its set of lower cuts, and the upper Dedekind completion of an upper duiq is its set of upper cuts.
For example, let $X$ be a compactum and let $S$ be the quasiordered set of continuous real-valued functions on $X$. Then $S$ is a duiq, hence both a lower and upper duiq. Its lower Dedekind completion is the set of lower semicontinuous functions on $X$ taking values in the lower reals (which classically are all either real or $\infty$); and dually on the upper side. Even working classically and ignoring the technicality of $\infty$, semicontinuous functions are much more general than continuous ones.
Page 249&250 of Continuous Lattices and Domains (Google book) covers lower Dedekind completions of duiqs (although not under that name) in the context of domain theory.
Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
Auke B. Booij, Extensional constructive real analysis via locators, (arxiv:1805.06781)
Steve Vickers, “Localic Completion Of Generalized Metric Spaces I”, TAC
Davorin Lešnik, Synthetic Topology and Constructive Metric Spaces, (arxiv:2104.10399)
Last revised on May 10, 2022 at 09:28:09. See the history of this page for a list of all contributions to it.