philh comments on Löb’s Lemma: an easier approach to Löb’s Theorem

[philh]

Thanks, that makes sense. And the added explanation helps a lot, I can see the argument for going from $⊢A\to B$ to $A⊢B$ now:

• PA proves $A\to B$;

• So PA + $A$ certainly proves $A\to B$, since it can prove everything PA can;

• Also, PA + $A$ proves $A$;

• So we have $A⊢A\wedge (\neg A\vee B)$;

• Which in turn gives us $A⊢B$.