You can’t write down ‘∀p: Provable(p)→p’ in PA, because in order to quantify over sentences we have to encode them as numbers (Gödel numbering).
We do have a formula Provable, such that when you substitute in the Gödel number p you get a sentence Provable(p) which is true if and only if the sentence p represents is provable. But we don’t have a formula True, such that True(p) is true if and only if the sentence p represents is true. So the unadorned p in ‘∀p: Provable(p)→p’ isn’t possible. No such formula is possible since otherwise you could use diagonalization to construct the Liar Paradox: p⟷¬True(p) (Tarski’s undefinability theorem).
What we can do is write down the sentence ‘Provable(p)→p’ for any particular Gödel number p. This is possible because when p is fixed we don’t need True(p), we can just directly use the sentence p represents. I think of this as a restricted version of soundness: ‘Soundness at p’. Then Löb’s theorem tells us precisely which p PA is sound at. It’s precisely the p which PA can prove.
You can’t write down ‘∀p: Provable(p)→p’ in PA, because in order to quantify over sentences we have to encode them as numbers (Gödel numbering).
We do have a formula Provable, such that when you substitute in the Gödel number p you get a sentence Provable(p) which is true if and only if the sentence p represents is provable. But we don’t have a formula True, such that True(p) is true if and only if the sentence p represents is true. So the unadorned p in ‘∀p: Provable(p)→p’ isn’t possible. No such formula is possible since otherwise you could use diagonalization to construct the Liar Paradox: p⟷¬True(p) (Tarski’s undefinability theorem).
What we can do is write down the sentence ‘Provable(p)→p’ for any particular Gödel number p. This is possible because when p is fixed we don’t need True(p), we can just directly use the sentence p represents. I think of this as a restricted version of soundness: ‘Soundness at p’. Then Löb’s theorem tells us precisely which p PA is sound at. It’s precisely the p which PA can prove.
Then apparently “PA can’t prove its own soundness.” is an even weaker true statement among the ones one might choose to remember :).