Solution (source code)

= Solution

\b[<Rice theorem>: every nontrivial <extensional property of programs> computing <partial computable functions> has an undecidable <index set>.] More precisely, take an acceptable effective enumeration $(\varphi_e)$ of the unary <partial computable functions>. If $\mathcal P$ contains some but not all of these functions, then
$$
\boxed{I_{\mathcal P}=\{e:\varphi_e\in\mathcal P\}\text{ is not computable.}}
$$
“Extensional” means that equality of <partial functions>, including their domains, preserves membership; no syntactic restriction on program codes is being considered.

We use two standard facts, stated explicitly. The <diagonal halting set> $K=\{e:\varphi_e(e)\downarrow\}$ is undecidable. For the associated acceptable enumerations $\varphi_e^{(r)}$ of $r$-ary <partial computable functions>, with $\varphi_e=\varphi_e^{(1)}$, the <S-m-n theorem> says that for every $m,n\geq1$ there is a <total computable function> $s_n^m$ such that
$$
\varphi_{s_n^m(e,x_1,\ldots,x_m)}^{(n)}(y_1,\ldots,y_n)
\simeq\varphi_e^{(m+n)}(x_1,\ldots,x_m,y_1,\ldots,y_n),
$$
where $\simeq$ means equality of defined values and equality of undefinedness. Thus fixed parameters in a program can be compiled into its index effectively.

Let $\bot$ be the nowhere-defined <partial computable function>. Choose a <partial computable function> $h$ whose membership in $\mathcal P$ is opposite to that of $\bot$; this is possible by nontriviality. For each $e$, construct the program
$$
\psi_e(y):\quad\text{first simulate }\varphi_e(e);
\quad\text{if it halts, simulate }h(y)\text{ and return its value}.
$$
This is a uniform partial computation. Take an index $d$ for the binary <partial computable function> $(e,y)\mapsto\psi_e(y)$. The <S-m-n theorem> gives the <total computable function> $q(e)=s_1^1(d,e)$ with $\varphi_{q(e)}=\psi_e$. Crucially,
$$
\psi_e=\begin{cases}h,&e\in K,\\\bot,&e\notin K.\end{cases}
$$
Even when $h(y)$ itself is undefined, the equality of <partial functions> remains correct. If $\bot\notin\mathcal P$, this gives a <many-one reduction> of $K$ to $I_{\mathcal P}$; if $\bot\in\mathcal P$, it gives a <many-one reduction> of $K$ to the complement of $I_{\mathcal P}$. A decision procedure for $I_{\mathcal P}$ would therefore decide $K$ in either case, a contradiction.

The equivalent language formulation says that every nontrivial property of <computably enumerable languages> depending only on the recognized language has an undecidable <index set>. Apply the function formulation to the property of a <partial computable function> that its domain has the specified language property: every <computably enumerable language> occurs as such a domain.