# 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 problem. So, is there constructive proof?

-
Assuming that my answer is correct, together with Andrej Bauer's answer (which is certainly correct) it shows that you have to make your question more specific. How is the recursive set given? By a code for an enumeration, or by a code for its characteristic function? –  Goldstern Jan 8 '12 at 23:58
@Goldstern: it has to be the code of a characteristic function. If we had recursive sets given by codes of their enumerations, then constructively that would correspond to "countable subsets of $\mathbb{N}$ for which it is false to assume that they are not decidable", a rather convoluted notion. –  Andrej Bauer Jan 9 '12 at 0:17
(For the reader who did not see the history: my previous comment referred to Andrej's first answer, which pointed out that an enumeration -- even of a finite set -- cannot effectively be turned into an increasing enumeration.) –  Goldstern Jan 9 '12 at 0:22
Ah yes, I misread the question at first I thought we wanted non-decreasing enumerations of c.e. sets. Those can't be had, or else we sovle the Halting problem quite easily. –  Andrej Bauer Jan 9 '12 at 7:32

Here is Goldstern's answer, transcribed to constructive mathematics.

In constructive mathematics we do not speak of "recursive" but rather decidable subsets of $\mathbb{N}$. (Recall that a subset $X \subseteq Y$ is decidable if $\forall y \in Y. y \in X \lor y \not\in X$.) Also, your assumption that $A \neq \emptyset$ should be replaced with "$A$ is inhabited", i.e., $\exists n \in A . \top$, or else one is forced to use Markov principle unecessarily.

Let us also observe that an inhabited decidable subset $A \subseteq \mathbb{N}$ has a minimal element. Indeed, given $k \in A$, we may find the least $j \leq k$ such that $j \in A$ by simply checking all of them.

Suppose then that $A$ is a decidable inhabited subset of $\mathbb{N}$. We wish to enumerate the elements of $A$ in a non-decreasing order. Because $A$ is inhabited and decidable it has a minimal element $k \in A$. Now simply define an enumeration $e : \mathbb{N} \to A$ by $$e(n) = \max \lbrace i \in A \mid i \leq \max(n,k) \rbrace.$$ The maximum in the definition of $e$ exists because it is over a finite inhabited subset of $\mathbb{N}$. Clearly, $e(n) \in A$ for all $n$, and $e$ enumerates all of $A$ because $e(m) = m$ when $m \in A$.

-
Indeed, a much nicer and better readable formulation than mine. –  Goldstern Jan 9 '12 at 0:28

Given a program $P$ I can write a new program $f(P)$ that does the following:

• Let $k$ be the input for $f(P)$.
• Using an unbounded loop, find the first $n_0$ such that $P(n_0)=1$.
• If $k=0$, output $n_0$ and stop.
• Using a bounded loop, find the largest $i\le \max(n_0, k)$ such that $P(i)=1$.
• Output $i$ and stop.

So far I have only transformed a program $P$ into a new program $f(P)$ -- even constructivists or intuitionists will agree that my function $f$ is explicitly computable.

Now assume that $P$ computes the characteristic function of a recursive set $A$ (and is in particular total and outputs only 0 and 1). Then I claim that (constructively):

1. If $A$ is inhabited (i.e., there is some $n\in A$) then $f(P)$ is again total.

2. Every value $f(P)(k)$ is an element of $A$, i.e., $P(f(P)(k))=1$ for all $k$.

3. The function $f(P)$ is weakly monotone, i.e., $k\le k'$ implies $f(P)(k)\le f(P)(k')$. (I think that "weakly monotone" is not the same as "nondecreasing", constructively, but I assume that you meant "weakly monotone".)

4. Every $x\in A$ is a value of $f(P)$. In fact, $f(P)(x)$ first computes some value $n_0 \le x$, and then the largest $i \le x$ with $P(i)=1$, which is $x$ itself.

Note: If there is an enumeration of $A$, then $A$ must be inhabited. I think that being nonempty (i.e., "from $A=\emptyset$ we can get a contradiction") is not enough.

-