Comment by sasha on The Cartoon Guide to Löb's Theorem · 2008-08-17T22:28:52.000Z · LW · GW

Löb proved the following: for any C, Provable(Provable(C)->C)->Provable(C).

So, we may derive from PA soundness, that for any C, Provable(Provable(C)->C)->C.

Nobody proved, as you stated, that for any C (Provable(C)->C)->C.