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).
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)
Distribute the box over the second form: ◻L → (◻◻L → ◻C)
◻L also means ◻◻L since we can add boxes, so by the inference “A->(B->C) + (A->B) → (A->C)” we know ◻L → ◻C
All of that was standard PA. Here it becomes funny; Lob’s hypothesis tells us that ◻C can become C, so ◻L → C
Adding a box to that gives ◻(◻L->C), which in 1. we said was the same as ◻L
And in 4. we found out that ◻L gives C, so finally C
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).
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)
Distribute the box over the second form:
◻L → (◻◻L → ◻C)
◻L also means ◻◻L since we can add boxes, so by the inference “A->(B->C) + (A->B) → (A->C)” we know
◻L → ◻C
All of that was standard PA. Here it becomes funny; Lob’s hypothesis tells us that ◻C can become C, so
◻L → C
Adding a box to that gives ◻(◻L->C), which in 1. we said was the same as
◻L
And in 4. we found out that ◻L gives C, so finally
C