= Solution
<Rice's theorem>, in its <formal language> version, says: \b[every nontrivial property of the <computably enumerable language> accepted by a <Turing machine> has an <undecidable> set of machine descriptions.] Here nontrivial means that some <computably enumerable language> has the property and some does not. The property must be an <extensional property of programs>: any two <Turing machines> accepting the same <formal language> must agree about it. It need not be a property of all <formal languages>, including those no <Turing machine> accepts.
Let $\mathscr P$ be such a property and write
$$
I_{\mathscr P}=\{\operatorname{enc}(N):\mathcal L(N)\in\mathscr P\}.
$$
We prove the theorem by a <many-one reduction> from the <halting problem>. First suppose the <empty language> is not in $\mathscr P$. Nontriviality provides a fixed <Turing machine> $B$ with $\mathcal L(B)\in\mathscr P$. Given a <Turing machine> $M$ and a <word over an alphabet> $w$, effectively construct a <Turing machine> $N_{M,w}$ which, on <input> $x$, first simulates $M$ on $w$. If that simulation ever halts, it simulates $B$ on $x$ and accepts precisely when $B$ accepts. If the first simulation never halts, it never accepts $x$.
The <Turing machine encoding> of $N_{M,w}$ is computable from those of $M,w$: the description merely embeds $M,w$ and the fixed simulator for $B$. Constructing it does not require predicting whether $M$ halts. Its accepted <formal language> is
$$
\mathcal L(N_{M,w})=
\begin{cases}
\mathcal L(B),&M\text{ halts on }w,\\
\varnothing,&M\text{ does not halt on }w.
\end{cases}
$$
Consequently
$$
M\text{ halts on }w\quad\Longleftrightarrow\quad
\operatorname{enc}(N_{M,w})\in I_{\mathscr P}.
$$
A decider for $I_{\mathscr P}$ would therefore decide the <halting problem>, a contradiction. Invalid descriptions can be mapped to a fixed description of a machine accepting the <empty language>, if the <many-one reduction> is formulated on all <strings>.
If the <empty language> does belong to $\mathscr P$, apply the preceding argument to the opposite property, within the <computably enumerable languages>. This opposite property is still nontrivial and excludes the <empty language>. A hypothetical decider for $I_{\mathscr P}$ would decide the opposite property's index set by first rejecting malformed <Turing machine encodings> and otherwise reversing its answer. The opposite property is <undecidable> by the first case, giving the required contradiction in this case too.
$$
\boxed{I_{\mathscr P}\text{ is undecidable for every nontrivial extensional }\mathscr P.}
$$
Back to article page
