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.
Current theme: default
Less Wrong (text)
Less Wrong (link)
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.