A non-mechanical way to get an infinite decidable subset of a Turing-recognizable language? There's a famous theorem that every infinite Turing-recognizable language has an infinite decidable subset. The standard proof of this result works by constructing an enumerator for the Turing-recognizable language, then including the first enumerated string in the decidable language, then the first string that comes after it lexicographically, then the first string that comes after that lexicographically, etc. Since this set is enumerated by a Turing machine in lexicographically increasing order, it's decidable.

This construction works, but it doesn't seem to give a very "natural" example of an infinite decidable subset. In particular, the only way I can think of to describe the subset is to point at a specific enumerator for the language, define a recurrence relation from it, and then define the language from that recurrence relation.

Is there an alternative construction that produces an infinite decidable set from an infinite Turing-recognizable language that is less dependent on the particulars of how a specific enumerator runs?
Let $\Sigma$ be an alphabet, let $\mathcal{R}$ be the collection of all recognizable subsets (languages) of $\Sigma^{*}$ and let $\mathcal{D}$ be the collection of all decidable subsets of $\Sigma^{*}$.

Say that $n \in \mathbb{N}$ is a code for $L \in \mathcal{R}$ if the Turing machine encoded by the number $n$ (via some Gödel encoding of Turing machines) recognizes $L$. Let us write $L_n$ for the set that is recognized by the $n$-th Turing machine.

Similarly, say that $n$ is a code of $D \in \mathcal{D}$ if the $n$-th Turing machine is the decider for $D$. If $n$ is the code of a decider (not every number is!) then we write $D_n$ for the set it decides.

Consider the statement: "For every infinite $L \in \mathcal{R}$ there is an infinite $D \in \mathcal{D}$ such that $D \subseteq L$."

You are asking whether we can prove the statement by giving an effective procedure which assigns to every $L$ a corresponding $D$ in such a way that $D$ does not depend on the choice of the code of $L$. (Clearly, we can do this inefectively by an application of the axiom of choice.) More precisely, the question seems to be whether there a computable map $f$ such that


if $n$ codes an infinite $L \in \mathcal{R}$ then $f(n)$ codes an infinite $D \in \mathcal{D}$ such that $D \subseteq L$, and
if $L_n = L_m$ then $D_{f(n)} = D_{f(m)}$.


The answer is no, there is no such map: you must appeal to a particular recognizer for $L$ and obtain a $D$ which depends on the recognizer.

To prove that this is really so we appeal to Rice's theorem. Suppose we had such an $f$. There exists $n, m, a \in \mathbb{N}$ such that $a \in D_n$ and $a \not \in D_m$. The subset $S \subseteq \mathcal{R}$ defined by
$$L \in S \iff \exists n \,.\, L = L_n \land a \in D_{f(n)}$$
is a non-trivial decidable subset of $\mathcal{R}$, which violates Rice's theorem.