Anatoly_Vorobey 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)
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.