Is the set of undecidable problems decidable?

Question

I would like to know if the set of undecidable problems (within ZFC or other standard system of axioms) is decidable (in the same sense of decidable). Thanks in advance, and I apologize if the question is too basic.

Answer 1

No, in fact the situation is even worse than that. The set $T$ of all (Gödel codes for) sentences that are provable from ZFC is computably enumerable; the set $F$ of all sentences that refutable from ZFC is also computably enumerable. These two sets $T$ and $F$ form an inseparable pair: $T \cap F = \varnothing$ but there is no computable set $C$ such that $T \subseteq C$ and $F \cap C = \varnothing$.

In other words, there is no finite algorithm that can reliably tell whether a sentence is "not provable" or "not refutable." This is much weaker than asking for an algorithm to tell us whether a sentence is independent or not (in which case we could determine whether it is provable or refutable by waiting until it enters $T$ or $F$).

This remains true if ZFC is replaced by PA and some still weaker theories.

Answer 2

For every consistent recursively axiomatizable theory $T$ (one of which $ZFC$ is widely believed to be) there exists an integer number $K$ such that the following Diophantine equation (where all letters except $K$ are variables) has no solutions over non-negative integers, but this fact cannot be proved in $T$:

\begin{align}&(elg^2 + \alpha - bq^2)^2 + (q - b^{5^{60}})^2 + (\lambda + q^4 - 1 - \lambda b^5)^2 + \\ &(\theta + 2z - b^5)^2 + (u + t \theta - l)^2 + (y + m \theta - e)^2 + (n - q^{16})^2 + \\ &((g + eq^3 + lq^5 + (2(e - z \lambda)(1 + g)^4 + \lambda b^5 + \lambda b^5 q^4)q^4)(n^2 - n) + \\ &(q^3 - bl + l + \theta \lambda q^3 + (b^5-2)q^5)(n^2 - 1) - r)^2 + \\ &(p - 2w s^2 r^2 n^2)^2 + (p^2 k^2 - k^2 + 1 - \tau^2)^2 + \\ &(4(c - ksn^2)^2 + \eta - k^2)^2 + (r + 1 + hp - h - k)^2 + \\ &(a - (wn^2 + 1)rsn^2)^2 + (2r + 1 + \phi - c)^2 + \\ &(bw + ca - 2c + 4\alpha \gamma - 5\gamma - d)^2 + \\ &((a^2 - 1)c^2 + 1 - d^2)^2 + ((a^2 - 1)i^2c^4 + 1 - f^2)^2 + \\ &(((a + f^2(d^2 - a))^2 - 1) (2r + 1 + jc)^2 + 1 - (d + of)^2)^2 + \\ &(((z+u+y)^2+u)^2 + y-K)^2 = 0. \end{align}

The set of numbers with this property is not recursively enumerable (let alone decidable). But curiously enough, one can effectively construct an infinite sequence of such numbers from the axioms of $T$.

The equation is derived from Universal Diophantine Equation by James P. Jones.

Answer 3

I believe that one can expand on boumol's answer, as follows.

The spirit of the OP's question attempts to regain Eden after the Turing-Godel expulsion.

One might attempt to repair the OP's attempt in a more general way by adjusting the mathematician's aim from settling questions (with a proof of either yes or no) to resolving questions (say, with proof of yes, or no, or independence (relative to consisistency), independence of independence, etc). One can even allow, in many different ways, stronger and stronger reasonable axioms (iterated consistency or reflection principles) as one pursues all these statements of iterated independence.

Trouble always ensues because a programmer can always dovetail a countable number of uniformly specified computer searches, making the program terminate if any one of those searches turns out successful.

Then having every formula in the theory fall into one class or another again makes the set of consequences of ZFC decidable, contradiction.