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
inaccessible cardinal is weakly decidable.
The original question can then be rephrased as, are some statements not even weakly decidable ?
 A: 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.

*

*$ ZFC \vdash Con(ZFC) \Rightarrow T_n\text{ halts}$
In this case, it must be true that $T_n$ halts.


*$ ZFC \vdash Con(ZFC) \Rightarrow \neg(T_n\text{ halts})$
In this case it must be false that $T_n$ halts.


*$ 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.
