Skip to main content
1 of 4
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

I am going to answer twice. Once as if your use of the word "constructive" meant "computable", and once as if it actually meant "constructive" in the sense of "constructive mathematics".

First answer: Suppose there were a computable method $c$ of transforming (codes of) computable enumerations of non-empty sets to non-decreasing computable enumerations of non-empty sets. Then we can solve the Halting oracle as follows. Given any Turing machine $T$, consider the sequence $e : \mathbb{N} \to \mathbb{N}$ defined by $$e(n) = \begin{cases} 1 & \text{$T$ does not halt at step $n$} \\\\ 0 & \text{$T$ halts at step $n$} \end{cases}$$ The map $e$ enumerates the set $\{0,1\}$ or $\{1\}$, depending on whether $T$ halts. By assumption $c$ transforms $e$ into a non-decreasing enumeration $e'$ which enumerates the same set as $e$. If $e'(0) = 0$ then $T$ halts, otherwise it does not.

Second answer: In constructive mathematics we can just drop the adjetive "computable" from "computable enumeration". Suppose for every enumeration $e : \mathbb{N} \to \mathbb{N}$ there existed another enumeration which listed the same elements in non-decreasing order. We can derive from this the non-constructive principle LPO as follows. Consider a map $f : \mathbb{N} \to \{0,1\}$. We are supposed to decide whether $\exists n \in \mathbb{N} . f(n) = 0$. By assumption there is a non-decreasing map $e' : \mathbb{N} \to \mathbb{N}$ which has the same image as $f$. We simply look at $e'(0)$ to tell whether $f$ attains $0$.

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239