About the decidability of sets enumerated in non decreasing order It is well known that a set of numbers enumerable in nondecreasing order is
decidable. However, the typical proof, by cases on the finiteness of the
enumerated set, is not constructive. In general, it does not seem possible
to effectively derive the decider from the enumeration function (and its properties): can this be proved?

Here is a possible formalization of the problem. Let $\varphi$ be an effective enumeration of all computable functions.
Let $c_A$ be the characteristic function of $A$, Let $f$ be a function such that

$$\varphi_{f(i)} =
\begin{cases}
c_{cod{(\varphi_i})} &amp; \mbox{if $\varphi_i$ is total and non decreasing}\\
                 \mbox{arbitrary} &amp; \mbox{otherwise}
\end{cases}
$$
Prove that no such $f$ is computable (or that it is indeed computable).
Suppose there were a computable $f$ as described in the question. Then we could solve the Halting problem as follows.

Given a Turing machine $T$, consider the computable function $g$, defined by
$$g(k) = \begin{cases}
1 &amp; \text{if $T$ halts in $\leq k$ steps} \\
0 &amp; \text{otherwise}
\end{cases}$$
This is a computable, nondecreasing and total function. Therefore, we may use $f$ to establish that the range of $g$ is decidable. But now we just check whether $1$ is in the range to figure out whether $T$ halts.

Notice that I never used the finite/infinite distinction. The above argument works even if we assume that $f$ enumerates a finite set. Are you sure you got your theorem correct? The one I know says that an infinite set is decidable if it can be enumerated by a computable strictly increasing function. There is of course another theorem stating that every finite set can (obviously) be enumerated in increasing order.

Supplemental: Let us look at the matter from a constructive point of view. We have two constructive theorems, assuming Markov principle (which is generally used in computability theory):


  Theorem 1: If a finite set can be enumerated in non-decreasing order then it is decidable.


(A set is said to be finite if it is isomprhic to $\{0, 1, \ldots, n-1\}$ for some $n \in \mathbb{N}$, so the extra conditions in the theorem does not actually help, as every finite set is decidable.)


  Theorem 2: If a non-finite set can be enumerated in non-decreasin order then it is decidable.


However, we cannot just stick these two together into "any set enumerated in increasing order is decidable" because the following is not a constructive theorem:


  Theorem (classical): Every set is finite or non-finite.


In fact, in computability theory there are counter-examples. An immune set is infinite, but it does not contain any infinite computable sequence.