Is there a known example of a set $S$ of Diophantine equations such that


1. $S$ is computable;
2. it is a theorem that every equation in $S$ has (at most) finitely many solutions;
3. the function that maps an element of $S$ to its set of solutions is uncomputable?


There are some famous finiteness theorems in number theory whose proofs are ineffective; e.g., Faltings's theorem that a curve of genus at least 2 has at most finitely many rational points, but in the examples I can think of, there is no proof that an algorithm does not exist—we just don't know of one.


By the way, although I said "Diophantine equations"—implying integer solutions—I'd be satisfied with an example where we're considering solutions in some other ring with a countably infinite number of elements (e.g., $\mathbb{Q}$).



Hilbert's tenth problem for equations with finitely many solutions
Yes (assuming that you're representing finite sets in an appropriately canonical manner). The proof of the MRDP theorem gives a stronger result: there is a computable function $f$ such that, for every $e$, the c.e. set $W\_e$ is equal to the $f(e)$th Diophantine set $D\_{f(e)}$ (in some fixed standard enumerations of each). This lets us transfer all the usual undecidability results around properties of c.e. sets to properties of Diophantine sets.


In particular, the fact that there is a computable sequence of indices for finite c.e. sets such that the corresponding sequence of *canonical* indices for *finite* sets is not computable gives the result you want.


