You are entirely correct; I don’t know why I was confused.
However, looking at the proof again, it seems there might be a potential hole. You use Löb’s theorem within an assumption sub-loop. This seems to assume that from “A→(□B→B)”, we can deduce “A→B”.
But this cannot be true in general! To see this, set A=□B→B. Then A→(□B→B), trivially; if, from that, we could deduce A→B, we would have (□B→B)→B for any B. But this statement, though it looks like Löb’s theorem, is one that we cannot deduce in general (see Eliezer’s “medium-hard problem” here).
Can this hole be patched?
(note that if A→(□AB→B), where □A is a PA proof that adds A as an extra axiom, then we can deduce A→B).
You are entirely correct; I don’t know why I was confused.
However, looking at the proof again, it seems there might be a potential hole. You use Löb’s theorem within an assumption sub-loop. This seems to assume that from “A→(□B→B)”, we can deduce “A→B”.
But this cannot be true in general! To see this, set A=□B→B. Then A→(□B→B), trivially; if, from that, we could deduce A→B, we would have (□B→B)→B for any B. But this statement, though it looks like Löb’s theorem, is one that we cannot deduce in general (see Eliezer’s “medium-hard problem” here).
Can this hole be patched?
(note that if A→(□AB→B), where □A is a PA proof that adds A as an extra axiom, then we can deduce A→B).