Comment by kallisti on Löb's theorem simply shows that Peano arithmetic cannot prove its own soundness · 2021-04-22T09:50:13.680Z · LW · GW

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.\forall p(PA⊢(Prov\left(p\right)\to p\left)\right)\to (PA⊢p))$ (Löb's theorem)

$2.\forall p\left(\neg \right(PA⊢p)\to \neg (PA⊢\left(Prov\right(p)\to p)\left)\right)$ (Contraposition)

$3.\exists p\neg (PA⊢p)$ (e.g., 1 + 1 = 3)

$4.\exists p\neg (PA⊢(Prov\left(p\right)\to p\left)\right)$ (from 2)

$5.\neg \forall p(PA⊢(Prov\left(p\right)\to p\left)\right)$ (by change of quantifiers)