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

Larry_D'Anna 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: Larry_D'Anna 18 August 2008 03:35:02PM 6 points [-]

Eliezer: "Larry, interpret the smiley face as saying:

PA + (◻C -> C) |-"

OK ignoring the fact that this is exactly what it doesn't say, I suppose we could notice that every step is surrounded at the top by a happy-face-says, so, if we may be inclined to think we can take those off and get a proof inside PA, starting with "◻C -> C" as a hypothesis. Lets see what happens.

1. ◻L <-> ◻(◻L -> C) 2. ◻C -> C

ok these are our hypothesis.

3. ◻(◻L->C) -> (◻◻L -> ◻C)

Modus Ponens works in PA, fine

4. ◻L -> (◻◻L -> ◻C)

ordinary MP

5. ◻L -> ◻◻L

if PA can prove it, then PA can prove it can prove it

6. ◻L -> ◻C

ordinary MP

7. ◻L -> C

ordinary MP

8. ◻(◻L -> C)

ARGH WHAT ARE YOU DOING. THERE IS NO RULE OF FIRST ORDER LOGIC THAT ALLOWS YOU TO DO THIS. TO SAY "if i can prove X then i can prove i can prove X" STEPS OUTSIDE OF FIRST ORDER LOGIC YOU LOSE.

9. ◻L

ordinary MP

10 C

ordinary MP