# Is there constructive proof of the fact that every recursive set $A \ne \varnothing$ is recursively enumerable in non-decreasing order?

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?

-

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.

-
How do you distinguish between "nonempty" and "inhabited" here? Is it something like $\neg\neg\exists x\in A$ versus $\exists x\in A$? – Henning Makholm Jan 9 '12 at 23:25
@Henning: Yes, that is exactly the difference. Constructivists tend to use "nonempty" to mean the former, and "inhabited" the latter. The difference between them is a special case of "Markov's principle". – Carl Mummert Jan 10 '12 at 1:37
By the way, funny how the asker at MO and the one here have identical gravatars... – Henning Makholm Jan 10 '12 at 15:40