# iterated unprovability

Hi all the following might be a silly question

it is well known that some statements like for example CH are not provable within ZFC (assuming consistency of course) ie. $ZFC\not\vdash CH$. However, CH is not so bad in the sense that at least its unprovability is provable ie. $ZFC\vdash Con(ZFC) \to \ulcorner ZFC\not\vdash CH\urcorner$ or given a formalized provability predicate $\mathsf{proof}(x)$ that $ZFC\vdash Con(ZFC) \to \neg\mathsf{proof}(\ulcorner CH\urcorner)$. Coming to my question:

for any formula $A$ let $A[n]$ be defined from \begin{align*} A[0] &= A\\ A[n+1] &= Con(ZFC)\to \neg \mathsf{proof}(\ulcorner A[n]\urcorner) \end{align*}

for example $CH[0]$ is not provable, but $CH[1]$ is provable and all following $CH[n]$ are provably wrong (I guess). Is there any known classification of which formulas $A$ for which natural number $n$ makes $A[n]$ provable?

• It is not true that ZFC proves $\lnot \text{pvbl}(\text{CH})$. If ZFC could prove that, ZFC could prove $\text{Con}(\text{ZFC})$, which it cannot by the second incompleteness theorem. There is no formula $\phi$ for which ZFC can prove $\lnot \text{pvbl}(\phi)$, when pvbl is a formalized provability predicate for ZFC. – Carl Mummert Dec 12 '15 at 13:41
• indeed quite obviousely so! what about ZFC proves con(ZFC) -> ¬(ZFC proves CH) – D.F.F Dec 12 '15 at 14:18