Larry_D'Anna comments on The Cartoon Guide to Löb’s Theorem

[Larry_D'Anna]

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.

1. ◻(◻L->C) → (◻◻L → ◻C)

Modus Ponens works in PA, fine

1. ◻L → (◻◻L → ◻C)

ordinary MP

1. ◻L → ◻◻L

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

1. ◻L → ◻C

ordinary MP

1. ◻L → C

ordinary MP

1. ◻(◻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.

1. ◻L

ordinary MP

10 C

ordinary MP

[[deleted]]

I tried summarizing it independently and came up with fewer steps and more narrative. Hope you don’t me replying here or stealing your lovely boxes.

PA lets us distribute boxes across arrows and add boxes to most things. Lob’s hypothesis says we can remove boxes (or at least do around statement C in the following).

1. L is defined (in a difficult, confusing, self-referential way that this margin is to narrow to contain) such that
   ◻L is equivalent to ◻(◻L → C)

2. Distribute the box over the second form:
   ◻L → (◻◻L → ◻C)

3. ◻L also means ◻◻L since we can add boxes, so by the inference “A->(B->C) + (A->B) → (A->C)” we know
   ◻L → ◻C

4. All of that was standard PA. Here it becomes funny; Lob’s hypothesis tells us that ◻C can become C, so
   ◻L → C

5. Adding a box to that gives ◻(◻L->C), which in 1. we said was the same as
   ◻L

6. And in 4. we found out that ◻L gives C, so finally
   C