The existence of unprovably unprovable statements provable in ZFC [duplicate]

Question

This question already has an answer here:

• Can unprovability unprovable? Is there an $\omega$-fold unprovability? 4 answers

I am aware of Gödel's second incompleteness theorem, the proven existence of several unprovable statements (in ZFC), and the possibility that a formal system may include statements that are unprovably unprovable, that is, that there are statements in them which cannot be proven by them, but additionally, they cannot even be proven to be unprovable by them. My question is this:

Can the existence of unprovably unprovable statements be proven/disproven in ZFC or a (not necessarily conservative) extension like TG or MK?

(I am aware of a similar question which asks if there can be unprovably unprovable statements in formal systems, however this asks if the existence of such statements is provable in ZFC, which is a different matter)

Answer 1

If a statement of the form

Such-and-such Turing machine never halts.

is independent of your favorite axiom system (that extends Robinson's Q), then it is true in $\mathbb N$.

Therefor a proof that it is independent would also prove that the machine doesn't halt.

And ZFC certainly proves that there are machines that can neither be proved to halt nor proved not to halt (otherwise searching for such a proof would constitute a decision procedure for the halting problem, which we know can't exist).

Putting these together, ZFC proves that if ZFC is consistent, then there exist statements of the above form that are independent of ZFC but cannot be proved to be independent.