Skip to main content
3 of 4
added 106 characters in body
Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239

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

Andrej Bauer
  • 48.8k
  • 11
  • 131
  • 239