Eliezer_Yudkowsky 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)
Larry, interpret the smiley face as saying:
PA + (◻C -> C) |-
Then the steps 1-10 of Lob's proof would seem to take us from:
PA + (◻C -> C) |- (◻C -> C)
to
PA + (◻C -> C) |- C
If this were the case, the deduction theorem would in fact come into play and give us:
PA |- (◻C -> C) -> C
So there must be at least one step of the reasoning 1-10 that does not apply. Which one and why?