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

Question

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?

Answer 1

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$.

Answer 2

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.