Every proof I've read about this fact considers two cases: $A$ - finite and $A$ - infinite but this is undecidable. So, is there constructive proof?
Is there constructive proof of the fact that every recursive set $A \ne \varnothing$ is recursively enumerable in non-decreasing order?
2 Answers
How about: $f(n) = \cases{\max \{i\in A\mid i \le n\} & \text{if }n \ge \min A\\ \min A & \text{otherwise}}$ where $f(0) \le f(1) \le f(2) \le f(3) \ldots$ enumerate $A$.
This can be computed by counting $n$ downwards until an element of $A$ is found. If we hit $0$, switch to counting upwards to find the minimum instead.
This was very recently asked on MathOverflow in this question. The answer is that, no, it cannot be proved constructively if phrased as "every nonempty decidable subset of $\mathbb{N}$" but the similar result "every inhabited decidable subset of $\mathbb{N}$ can be enumerated in nondecreasing order" can be proved constructively. (At the very least, it will come down to the exact definition of "constructively", and exactly what principles are allowable.) There are many delicate issues of this sort when we try to move from classical recursion theory to constructive mathematics.
Separately, the classical result "every nonempty recursive set can be enumerated in nondecreasing order" can be proved in a completely uniform way, there is no need for cases. What I mean by this is that there is a computable function $f$ that takes an index $e$ that decides membership in the computable set and returns an index $f(e)$ of a non-decreasing enumeration of the set. The index $f(e)$ simply checks whether $\phi_e(0) = 1$, then whether $\phi_e(1) = 1$, then whether $\phi_e(2) = 1$, and so forth, and enumerates in order the $i$ such that $\phi_e(i) = 1$. This is not much different than the method given by Henning Makholm in his answer.
The fact that the classical result can be proved in this uniform way follows, actually, from the fact that the modified version is provable constructively in the way that it is.
-
0By the way, funny how the asker at MO and the one here have identical gravatars... – 2012-01-10