So, I might be getting something wrong, but why doesn’t Löb’s theorem imply that statement? A semi-formal argument, skipping some steps:

1.∀p(PA⊢(Prov(p)→p))→(PA⊢p)) (Löb’s theorem)

2.∀p(¬(PA⊢p)→¬(PA⊢(Prov(p)→p))) (Contraposition)

3.∃p¬(PA⊢p) (e.g., 1 + 1 = 3)

4.∃p¬(PA⊢(Prov(p)→p)) (from 2)

5.¬∀p(PA⊢(Prov(p)→p)) (by change of quantifiers)

Yes, but 3 is a one-way street. You should remember the theorem, not the corollary.

So, I might be getting something wrong, but why doesn’t Löb’s theorem imply that statement? A semi-formal argument, skipping some steps:

1.∀p(PA⊢(Prov(p)→p))→(PA⊢p)) (Löb’s theorem)

2.∀p(¬(PA⊢p)→¬(PA⊢(Prov(p)→p))) (Contraposition)

3.∃p¬(PA⊢p) (e.g.,

1 + 1 = 3)4.∃p¬(PA⊢(Prov(p)→p)) (from 2)

5.¬∀p(PA⊢(Prov(p)→p)) (by change of quantifiers)

Yes, but 3 is a one-way street. You should remember the theorem, not the corollary.