sasha

• sasha 17 Aug 2008 22:28 UTC

  6 points

  on: The Car­toon Guide to Löb’s Theorem

  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.