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)
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)