# 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/… – Eric Naslund Sep 17 '11 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. – Ewan Delanoy Sep 17 '11 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. – Zhen Lin Sep 17 '11 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. – Ewan Delanoy Sep 17 '11 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.

-
Well done! I wonder if this nonconstructive proof can be turned into a constructive one, in the vein of the famous Goedel sentence "I am not provable ..." – Ewan Delanoy Sep 17 '11 at 19:08
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)$". – Henning Makholm Sep 17 '11 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 '11 at 2:36
@JDH, is such a world even possible in principle? If ZFC+Con(ZCF) is not consistent, then $ZFC\vdash\neg Con(ZFC)$ directly by contradiction, which seems to preclude ZFC being consistent in the first place. – Henning Makholm Sep 18 '11 at 2:51
@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... – François G. Dorais Mar 8 '14 at 15:44