I found your suggestive example on wikipedia earlier. Sadly it was no more rigorous than your example, nor did it cite sources that have more rigor. I suspect

I found your suggestive example on wikipedia earlier. Sadly it was no more rigorous than your example, nor did it cite sources that have more rigor. I suspect the additional rigor is mostly a matter of showing why 'special knowledge' is not allowed. That is certainly where my main objection lies. The 'decider' should get to inspect the Turing machine, and hence be able to prove things about them. I do find it plausible that something similar to the halting problem makes it impossible, but proving that does not seem trivial. I also think a construction like: Take a binary sequence x_i where x=1 if 2i+1 is a perfect number, 0 otherwise. Make that into a real number x in the interval [0, 1] in the standard way. x here is certainly a computable real number. Now the question is, does x equal 0. The question 'do perfect odd numbers exist' is unanswered. If it were undecidable, then the above equality would be undecidable as well. It doesn't seem impossible to find a construction like the above, but for a known undecidable problem.