Is there some set of problems, for which determining if given problem is decidable or not is itself undecidable?
-
3$\begingroup$ What, if any, of the two occurrences of the word “decidable” in your post refer to algorithmic decidability of a set of finite strings, and what refer to unprovability and nonrefutability of a formula in a formal system? In the latter case, what is the system? $\endgroup$– Emil JeřábekCommented Aug 25, 2015 at 17:36
-
1$\begingroup$ Alternatively, what precisely do you mean by a "problem"? Do you mean a conjecture or do you mean a language (set of strings)? If the latter, how do you plan to describe a potentially infinite set of strings in a way that can be presented to a computer that only accepts finitely long inputs? $\endgroup$– Timothy ChowCommented Aug 25, 2015 at 20:46
2 Answers
I'll echo Emil, that I believe you have used the word 'decidable' in two different ways. My reading of the question is whether there is a set which is not computable but the incomputability of that set is not provable.
The set of theorems of ZFC is an example of this type. Assuming ZFC is consistent (which is what I believe to be the case), the set of theorems of ZFC is not computable. However, if ZFC were inconsistent, then every formula would be a theorem of ZFC and so the set of theorems of ZFC would be decidable. So, "the incomputability of the set of theorems of ZFC" has the same proof-theoretic status as "the consistency of ZFC," proven by ZFC if and only if ZFC is inconsistent.
Yes. Determining whether a certain Turing machine will halt is undecidable by any algorithm, so in particular it is undecidable by listing theorems in, say, ZFC. But if a certain TM does halt, then then this is easy (in principle) to verify, and in particular it must be a theorem in ZFC that it halts. So if we could determine which problems are decidable and which are undecidable, then we could determine whether a Turing machine will halt. But we can't.