Larry_D'Anna 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)
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