kallisti

• kallisti 22 Apr 2021 9:50 UTC

  2 points

  in reply to: Gurkenglas’s comment on: Löb’s the­o­rem sim­ply shows that Peano ar­ith­metic can­not prove its own soundness

  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)