Essentially, yes, but I believe the undecidability of Peano arithmetic (henceforth, PA) follows from the way the proof of Gödel's incompleteness theorem goes, rather than being a consequence of the fact that PA is incomplete. The proof (outlined below) starts by showing that PA can talk about computable relations, and goes on to show from this how you can construct an unprovable sentence. However, we can take a different approach to show that PA is undecidable: if PA can talk about computable relations, then you can formulate a sentence in the language of PA that is true if and only if a given algorithm halts / does not halt. (Briefly: An algorithm is the same thing as a computable partial function, and an algorithm halts on some input if and only if the corresponding partial function is defined on that input.) So if an algorithm can decide whether arbitrary sentences in PA are provable or not, we have an algorithm which solves the halting problem... but there are nonesuch. So the key point is that PA is rich enough to talk about computation. An essential ingredient for talking about computation is the ability to encode a pair of numbers as a number and the ability to recover the original pair from the encoding. It's not immediately clear to me that $+$ is insufficient to do this, but it's certainly plausible that you need at least two binary operations.
Here is a sketch of the proof of Gödel's first incompleteness theorem: First let's select a sufficiently powerful theory $T$, e.g. PA, and assume that it is a consistent theory, i.e. does not prove a contradiction.
- We show that we can encode formulae and proofs in the models of $T$.
- We show that $T$ is powerful enough to talk about computable relations.
- We show that there is a computable relation $\mathrm{Prf}(m, n)$ which holds if and only if $m$ encodes a valid proof of the sentence encoded by $n$.
- The above shows that there is a computable relation $Q(m, n)$ which holds if and only if $n$ encodes a formula $F(-)$ with one free variable and $m$ does not encode a valid proof of $F(n)$.
- So we can define a formula $P(x)$ by $\forall m. Q(m, x)$. This means $P(x)$ holds if and only if there is no valid proof of $F(x)$, assuming $x$ encodes a formula $F(-)$ with one free variable.
- But $P(-)$ is a formula with one free variable, and it can be encoded by some number $n$. So is the sentence $P(n)$ provable or not? Suppose it were. Then, that means $P(n)$ is true, so the theory asserts that there is no valid proof of $P(n)$ — a contradiction.
- So we are forced to conclude that the sentence $P(n)$ is not provable. This is the Gödel sentence which we wished to prove the existence of, so we are done.
Note I haven't said anything about whether $P(n)$ is actually true. It turns out there is some subtlety here. Gödel's completeness theorem tells us that everything that can be proven in a first-order theory is true in every model of that theory and that every sentence which is true in every model of a first-order theory can be proven from the axioms of that theory. With some stronger consistency assumptions, we can also show that $\lnot P(n)$ is also not provable in PA, and this means that there are models of PA where $P(n)$ is true and models where it is false.
The key point is that the phrases "$n$ encodes a formula ..." and "$m$ encodes a valid proof of ..." are strictly outside the theory. The interpretation of a particular number as a formula or proof is defined externally, and we only define it for "standard" numbers. The upshot of this is that in a model $\mathcal{M}$ of PA where $P(n)$ is false, there is some non-standard number $m \in \mathcal{M}$ which $\mathcal{M}$ "believes" is a valid proof of $P(n)$, but because it's non-standard, we cannot translate it into a real proof.
I don't agree with the general idea that $\mathrm{Con}(T)$ isn't meaningful in non-$\omega$-models of theories like $\mathsf{PA}$ and $\mathsf{ZFC}$. This is alluded to in some of the discussion of Artemov's paper on FOM, but I think it's worth an answer here, specifically to your question, 'Why is this theorem interpreted as "a theory cannot prove its own consistency"?' The short answer is that $M \models \mathrm{Con}(T)$ really does mean that $T$ is consistent 'internally' inside $M$.
The way in which $\mathrm{Con}(T)$ is meaningful is easier to see in the context of $\mathsf{ZFC}$, but a version of this is true in $\mathsf{PA}$ as well. A really important result in mathematical logic is Gödel's completeness theorem which says that a first-order theory has a model if and only if it is consistent in the sense of a syntactic proof calculus. This fact is of course provable in $\mathsf{ZFC}$, that is to say that $\mathsf{ZFC}$ proves
$$\forall T (\mathsf{Con}(T) \leftrightarrow \exists M \models T).$$
What's important here is that any model $M$ of $\mathsf{ZFC}$ is correct about satisfying individual formulas. That is to say, if $A$ is some structure in $M\models \mathsf{ZFC}$, the for any standard formula $\varphi(\bar{x})$ and any $\bar{a} \in A$, $M$ 'thinks' $A \models \varphi(\bar{a})$ if and only if $A \models \varphi(\bar{a})$. For infinite theories the issue of course is that there are now non-standard formulas, but you still get one direction, specifically, if $M \models \mathsf{ZFC}$ thinks that $A$ is a model of a computably enumerable theory $T$, then $A$ is actually a model of that theory.
$\mathsf{PA}$ and $\mathsf{ZFC}$ have the special property that they non-uniformly prove the consistency of any finite fragment of themselves. By a slightly tricky argument, this implies that every model of $\mathsf{ZFC}$ contains what is externally a model of $\mathsf{ZFC}$. In a model of $\mathsf{ZFC}+\neg\mathrm{Con}(\mathsf{ZFC})$, though, there is no way to definably separate these models from models of arbitrarily large finite fragments of $\mathsf{ZFC}$.
With finitely axiomatizable set theories like $\mathsf{NBG}$ or $\mathsf{NFU}$, Gödel's second incompleteness theorem has a far more striking implication. There are, for instance, models of $\mathsf{NFU}$ which contain no models of $\mathsf{NFU}$. $\mathsf{ZFC}$ has a similar phenomenon, which is that there are models of $\mathsf{ZFC}$ which contain no transitive models of $\mathsf{ZFC}$.
The analogous phenomenon with $\mathsf{PA}$ involves the fact that a certain form of the completeness theorem is provable in $\mathsf{PA}$: If a model $N$ of $\mathsf{PA}$ satisfies $\mathrm{Con}(T)$, then $N$ actually interprets the full elementary diagram of a model of $T$. The converse is true as well, so this means that a model $N$ of $\mathsf{PA} + \neg \mathrm{Con}(\mathsf{PA})$ does not interpret the full elementary diagram of a model of $\mathsf{PA}$.
Best Answer
Perhaps the most succinct answer is given by Hilbert in his article Über das Unendliche (On the Infinite):
Demonstration of self-consistency, together with completeness, is an indispensable requirement of Hilbert's programme on the whole of mathematics. Indeed, the fundamental roles of these two notions reasonably follow from his formalist vision of mathematics, that is, to put the point overly simply, an architecture that would describe mathematical objects and relations in their utmost generality, hence, in ideally abstract fashion.
Since the envisioned formal system would be bereft of any objects and relations that endow mathematical symbolism with meaning, thus traditionally serves as a guiding content against fallacies and defects, the system itself has to guide itself abiding by metamathematical principles and values. Gödel's incompleteness theorems show that both pillars of Hilbert's programme are unrealisable.
Of course, this could be an end to Hilbert's programme, but it is an important research topic to see to what extent a formal system accomplish within itself.