Löb's theorem simply shows that Peano arithmetic cannot prove its own soundness

I think you're right, the statement is intuitively soundness, but I'm still confused. I would be very grateful if you could clear it up. Is "soundness $\to$ consistency" what you mean by stronger? If we can assume necessitation, soundness and consistency are equivalent, proof below.

Does that mean we cannot assume the necessitation proof rule, that is if $⊢p$, add $⊢\square p$? This would be consistent with "PA cannot prove its own completeness", the necessitation rule would imply that completeness is true.

First, we prove that consistency implies soundness by modus tollens. Suppose no soundness: $\neg (\square p\to p)$; then $\square p\wedge \neg p$. From $\neg p$, by necessitation $\square \neg p$, and so overall $\square (p\wedge \neg p)$, that is $\square \perp$. We have proven $\neg (\square p\to p)\to \square \perp$, by modus tollens $\neg \square \perp \to (\square p\to p)$.

Second, we can prove that soundness implies consistency without necessitation, by modus tollens and contradiction. Suppose $\square \perp$. Further supposing $\square p\to p$ clearly proves $\perp$, so we reject the assumption, thus $\neg (\square p\to p)$. Thus we prove $\square \perp \to \neg (\square p\to p)$, by modus tollens $(\square p\to p)\to \neg \square \perp$.

Where did I go wrong? Is it the necessitation deduction rule? Is it that the necessitation deduction rule is valid, but cannot be used within a statement of PA?

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.

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)

In PA, when proving something, you get the lemma that it is provable for free

As I understand it, this verbal statement can be translated to $p\to \square p$, or at least $\square p\to \square \square p$. The first is false[1] (Gödel's 1st incompleteness theorem), the second is not obviously related to Löb's theorem.

[1] also related to necessitation, a proof rule that substitutes $\text{PA}⊢p$ for $\text{PA}⊢\square p$