LESSWRONG
LW

2038
kallisti
1010
Message
Dialogue
Subscribe

Posts

Sorted by New

Wikitag Contributions

Comments

Sorted by
Newest
No posts to display.
No wikitag contributions to display.
Löb's theorem simply shows that Peano arithmetic cannot prove its own soundness
kallisti4y20

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)

Reply