Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Anatoly_Vorobey comments on The Cartoon Guide to Löb's Theorem - Less Wrong

12 Post author: Eliezer_Yudkowsky 17 August 2008 08:35PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (92)

Sort By: Old

You are viewing a single comment's thread.

Comment author: Anatoly_Vorobey 18 August 2008 09:27:41PM 0 points [-]

Loeb's theorem shows that if PA proves "not P(C)->C", then PA proves C (using P(X) for "X is provable in PA").

It follows from that, using the Deduction Theorem, that PA proves "(not P(C)->C)->C"; it does _not_ follow that "(not P(C)->C)->C" is a logical tautology.

From that, you obtain, similarly, that PA proves "(not P(C)) -> C". And you say "I cannot prove that 2 = 1". Sure, you cannot, but can PA? That's the real question.

There's nothing particularly surprising about PA proving "(not P(C))->C". After all, were PA to prove "not P(C)" for any C, it would prove its own consistency, and therefore be inconsistent, and therefore prove C.