An example of an infinite family of problems (of questionable practical value) for which we can show:
- That for each problem there exists an algorithm to solve it.
- That there is no way to construct these algorithms (in general).
In other words, a provably non-constructive proof. Our family of problem (from this question) for each Turing machine $M$:
$L_{M}=\Bigl\{\langle M'\rangle \;\Big|\;\; L(M)=L(M') \text{ and } |\langle M\rangle| \geq | \langle M' \rangle| \Bigr\} $
For each $M$ this is a finite set, and thus decidable.
If we had a constructive proof $P$ (in a suitable formal system) that given a description of a Turing Machine $M$ generated a Turing Machine $P(\langle M \rangle)$ that decided $L_M$ then given two machines $M$ and $M'$ (with $|\langle M \rangle | \geq |\langle M' \rangle|$) then we could test for equality of the languages recognized by these machines by running $P(\langle M \rangle)(\langle M' \rangle)$. An impossibility by Rice's theorem; thus, such a constructive proof $P$ does not exist.
