Is there a constructive way to one-to-one associate elements $x\in\mathcal{P}\omega$ with elements ${\scriptstyle\mathbf I}\in\mathbf{I}\mathbb{R}$ ?
I assumed there should be since they're both universal (so kind of an embedding-embedding pair, so to speak), but haven't been able to figure out how it could be done, nor google a solution.

Edit: Re comment How do you constructively embed $\mathcal{P}(\{0,1,2\})$ into the interval domain?...
    Well, here's what I'd been thinking to do for $\mathcal{P}\omega$ in general, which doesn't work as a bijection, but which maybe vaguely works as an embedding. It's all kind of fast-and-loose in the spirit of Stoy's remark about "fiddling with sets of integers" (last paragraph on pg.116 in his book).
    First let's consider your definition $\mathbf{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R}_{[0,1]} \land a \leq b \}$ restricted to $\mathbb{R}_{[0,1]}=\{r\in\mathbb{R}\mid 0\leq r\leq1\}$. Then for $x\in\mathcal{P}\omega$, first, for each $i\in x$, use the inverse pairing function $\mathbb{N}\times\mathbb{N}\to\mathbb{N}$, e.g., https://en.wikipedia.org/wiki/Pairing_function, to get $x\to x_1,x_2$. Now use the usual construction $x\subseteq\mathbb{N}\to r_x=\sum_{i\in x}\frac1{2^i}\in\mathbb{R}_{[0,1]}$. So now we have $x\in\mathcal{P}\omega\to r_{x_1},r_{x_2}$, with which we associate the interval $[r_{_\mbox{lo}},r_{_\mbox{hi}}]$, choosing the lesser of $r_{x_1},r_{x_2}$ for $r_{_\mbox{lo}}$ and ditto for hi. And those $r$'s will be rational if $x$ is finite, and computable/constructive if it's r.e.
    Second, if it's really necessary to consider $\mathbb{R}$ rather than just $\mathbb{R}_{[0,1]}$, then for any $x\in\mathcal{P}\omega$, first get $x_1,x_2$ as above, but now separate each into its even and odd numbers, i.e., $x_1^e=\{\frac i2\mid i\in x_1\land i\mbox{ even}\}$ and $x_1^o=\{\frac{i+1}2\in x_1\mid i\mbox{ odd}\}$. And now use $x_1^e$ to determine the integer part of $r_{x_1}$ as $\sum_{i\in x_1^e}2^i$, and use $x_1^o$ to determine the decimal part as above.

  • 1
    $\begingroup$ Is this supposed to be an isomorphism of underlying sets (any bijection), or an isomorphism of posets (monotone), or an isomorphism of domains (continuous)? $\endgroup$ Nov 5, 2021 at 13:02
  • 1
    $\begingroup$ Sorry, I misread, you're looking for embeddings, not isomorphisms. $\endgroup$ Nov 5, 2021 at 14:25
  • 2
    $\begingroup$ Can you embed $P(\{0,1,2\})$ into $\mathrm{I}\mathbb{R}$? Also, please write down the exact definition of $\mathrm{I}\mathbb{R}$. $\endgroup$ Nov 5, 2021 at 14:55
  • 1
    $\begingroup$ Really? How do you constructively embed $P(\{0,1,2\})$ into the interval domain? And I think it's still important that you write down what you think the constructive interval domain is. Do you use Cauchy reals, Dedekind reals, or lower and upper Dedekind cuts? It may matter. $\endgroup$ Nov 6, 2021 at 8:30
  • 1
    $\begingroup$ Your edit is not using $\mathcal{P}(\omega)$ but $2^{\mathbb{N}}$. $\endgroup$ Nov 7, 2021 at 8:49

1 Answer 1


This is only half an answer, but allow me to clear up a constructive point about the interval domain.

The usual definition of the interval domain is $$\mathrm{I}\mathbb{R} = \{[a,b] \mid a, b \in \mathbb{R} \land a \leq b \} \cup \{\mathbb{R}\}, $$ ordered by reverse inclusion. If we try to use this definition constructively, we get stuck when showing that it is a dcpo. Even showng that an increasing sequence has a supremum is impossible (because constructively it may not be the case that a bounded increasing sequence of reals has a supremum).

The correct constructive definition of the interval domain goes as follows. An element of $\mathrm{I}\mathbb{R}$ is a pair $(L, U) \in P(\mathbb{Q}) \times P(\mathbb{Q})$ such that

  1. $L$ is lower and rounded: $p \in L \iff \exists q \in L \,.\, p < q$.
  2. $U$ is upper and rounded: $q \in U \iff \exists p \in U \,.\, p < q$.
  3. $L$ and $U$ are disjoint.

The ordering is defined by $$ (L,U) \sqsubseteq (L', U') \iff L \subseteq L' \land U \subseteq U'. $$ Think of $L$ and $U$ as the endpoints of the interval, given respectively as a lower and an upper Dedekind cut. Note that $\emptyset$ is allowed as a cut. It represents either $-\infty$ or $\infty$, for instance $(\emptyset, \emptyset)$ is the bottom element, $(\emptyset, U)$ represents an interval $(-\infty, u]$, and $(L, \emptyset)$ represents an interval $[\ell, \infty)$.

Clearly, we have an inclusion $\mathrm{I}\mathbb{R} \subseteq P(\mathbb{Q}) \times P(\mathbb{Q})$, and since $$ P(\mathbb{Q}) \times P(\mathbb{Q}) \cong P(\mathbb{Q} + \mathbb{Q}) \cong P(\omega), $$ we have an inclusion $\mathrm{I}\mathbb{R} \to P(\omega)$. The other direction I am still thinking about.

It is also quite clear that the two domains are not isomorphic posets, as $P(\omega)$ is an algebraic lattice but $\mathrm{I}\mathbb{R}$ is not.

Supplemental: I cannot tell from your question what precisely you are trying to do, but perhaps you will find Cartesian closed categories of separable Scott domains relevant. There we find invariants, namely coherence numbers, that determine when one universal domain embeds into another.

  • $\begingroup$ Thanks. Okay, I see your point that the computable subset of $\mathbf{I}\mathbb{R}$ won't be a subdomain (i.e., the "whether or not" part of my comment above should just be "not"). And thanks also for the more formal analysis than anything that had come to mind for me. It all makes me realize that I should have omitted "constructive" in the original question (I should maybe just be interested in the computable elements of each domain, and maybe an isomorphism between those subsets). $\endgroup$ Nov 7, 2021 at 7:57
  • 1
    $\begingroup$ That won't work either. The computable elements form effective domains (you get the c.e. sets instead of $P(\omega)$ and the computble interval domain). These are not computably isomorphic as domains because, again, one is algebraic and the other is not. $\endgroup$ Nov 7, 2021 at 8:47
  • 1
    $\begingroup$ Do you have an idea that any two universal domains ought to be isomorphic? Because that is not true. $\endgroup$ Nov 7, 2021 at 8:48
  • 1
    $\begingroup$ I linked to a paper that classifies universal separable Scott domains up to retraction, perhaps that will be relevant to your work. $\endgroup$ Nov 7, 2021 at 9:23
  • $\begingroup$ Re "idea that any two universal domains ought to be isomorphic": isomorphic is apparently too strong, but what had crossed my mind is that given any two universal domains $\mathcal{U}_1$ and $\mathcal{U}_2$, and any domain $D$, then there always exist retractions $\hat{r}_1:\mathcal{U}_1\to D$ and $\hat{r}_2:\mathcal{U}_2\to D$. So we can always say $\hat{r}_1\sim\hat{r}_2$ in some way, whereby the two collections of retractions are related in some way, hopefully a strong way, which hopefully extends to $\mathcal{U}_1$ and $\mathcal{U}_2$ themselves. But I hadn't carried this idea any further. $\endgroup$ Nov 8, 2021 at 6:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.