sasha comments on The Cartoon Guide to Löb's Theorem - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (90)
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.