# Are there statements that are undecidable but not provably undecidable

This is a variant of Is there a statement whose undecidability is undecidable? and Can it be shown that ZFC has statements which cannot be proven to be independent, but are? (but is not asked or answered in either of those threads).

Call a formula $\phi$ provably undecidable if $ZFC$ proves that ($ZFC$ is consistent) $\Rightarrow$ ($\phi$ is independent of ZFC). Now, (assuming that $ZFC$ is consistent) are there statements which are undecidable but not provably so ?

Here is another way to put it. Call a statement $\phi$ weakly decidable if ZFC can either prove that $\phi$ is true or prove that $\phi$ is false, or at least prove the implication ($ZFC$ is consistent) $\Rightarrow$ ($\phi$ is independent of ZFC).

Thus, the continuum hypothesis is weakly decidable in ZFC, and the axiom of choice is weakly decidable in ZF. On the other hand, it is not known today if the existence of an inacessible cardinal is weakly decidable.

The original question can then be rephrased as, are some statements not even weakly decidable ?

• I believe that this post on the linked thread answers your question: math.stackexchange.com/questions/17212/… Sep 17, 2011 at 10:08
• @Eric : I believe you're wrong, and that you did not notice the implication part in my definition. Of course I checked if the answer was not already in the linked thread. Sep 17, 2011 at 10:36
• Your definition is unclear. Of course ZFC can prove that $\phi$ is true or false. This is the law of excluded middle. And if ZFC can either prove $\phi$ or prove $\lnot \phi$ then $\phi$ is decidable. I'm confused. Sep 17, 2011 at 11:49
• @Zhen : sorry for the unclear english, I just corrected it : I meant "prove that $\phi$ is true or prove that $\phi$ is false", of course. The excluded middle is about truth, not provability. Sep 17, 2011 at 12:51

First assume that ZFC is indeed consistent. If every statement were either provably true or provably false or provably independent, then there would be a decision procedure that sorted all statements into these three groups -- just enumerate all valid proofs until one whose conclusion is one of the three forms were found.

We could use this to decide the halting problem. For any $$n$$ consider the statement "Turing machine $$T_n$$ halts". There are then three cases.

1. $$ZFC \vdash Con(ZFC) \Rightarrow T_n\text{ halts}$$

In this case, it must be true that $$T_n$$ halts.

2. $$ZFC \vdash Con(ZFC) \Rightarrow \neg(T_n\text{ halts})$$

In this case it must be false that $$T_n$$ halts.

3. $$ZFC \vdash Con(ZFC) \Rightarrow{}$$ "$$T_n$$ halts" is independent of ZFC.

In this case there must be a model of ZFC in which $$T_n$$ does not halt and so has an infinitely long computation. However, in every model of ZFC, the model's $$\omega$$ must contain a surjective image of the meta-$$\omega$$. (And similarly for whatever objects we use to represent Turing tapes). Therefore the infinite computation in the model corresponds to an infinite computation at the meta-level. Therefore $$T_n$$ really does not halt.

In conclusion, if ZFC is consistent, then your hypothesis leads to a solution to the halting problem, which we know is impossible. Thus by contradiction your hypothesis must be false if ZFC is consistent. On the other hand if ZFC is not consistent, then your hypothesis is still false, because then there are no unprovable statements at all.

• It is only superficially nonconstructive -- if you combine it it with the standard diagonalization argument for the nondecidabiliy of HALT, you should get a concrete statement that cannot be proved undecidable. In fact (if I've got all of the metalevels right), this would be closely equivalent to using Gödel's construction to produce a sentence that says "I am not provable from $ZFC+Con(ZFC)$". Sep 17, 2011 at 19:26
• It is not enough in your argument to assume only that ZFC is consistent. What you seem to need instead is that ZFC+Con(ZFC) is consistent. After all, if we are living in a world where ZFC+Con(ZFC) is true but Con(ZFC+Con(ZFC)) is not, then from a proof that Con(ZFC) implies a halt, you cannot deduce an actual halt.
– JDH
Sep 18, 2011 at 2:36
• Perhaps the philosophical view underlying your intuition is that whenever we are committed to a theory $T$, then of course we are naturally inclined also to accept Con(T) as well. So, accepting ZFC as true, we also accept Con(ZFC) and therefore also Con(ZFC+Con(ZFC)). It is kind of incoherent to accept the former and not the latter, but the incompleteness theorem shows that this greater commitment does not follow as a theorem. So there is ultimately this additional technical assumption in the argument.
– JDH
Sep 18, 2011 at 23:28
• @SébastienPalcoux The answer to my question is yes. Mar 7, 2014 at 14:59
• @JDH's objection is correct but there is more. The implicit assumption is actually that ZFC+Con(ZFC) is $\Sigma^0_1$-sound: that this theory does not prove any false $\Sigma^0_1$-statement. If ZFC+Con(ZFC) is not $\Sigma^0_1$-sound then there is a Turing machine $M$ such that ZFC + Con(ZFC) proves that "$M$ halts" but $M$ doesn't actually halt... Mar 8, 2014 at 15:44