Gödel's incompleteness theorem tells us that the language of first order arithmetic $PA_1$ is strong enough to express a statement about its own consistency, which cannot be proved in $PA_1$.
More generally if we take $PA_n$ to be $n$-th order arithmetic (that is we allow quantification over sets in $\mathcal P^n\mathbb N$), to what extent can we guarantee that if a formula $\phi$ is valid and can be stated in $PA_n$, then it has a proof in $PA_{f(n)}$?
Is there a common terminology for such "relative" completeness results?
The completeness theorem - also due to Godel! - says that this always happens, at least for first-order theories:
This does not contradict the incompleteness theorem. That result says that $PA_1$ is not a complete theory: there is a sentence (indeed, lots of sentences) $\sigma$ such that $PA_1\not\vdash\sigma$ and $PA_1\not\vdash\neg\sigma$, or equivalently by the completeness theorem $PA_1\not\models\sigma$ and $PA\not\models\neg\sigma$. The term "(in)complete" is being overloaded here:
A theory is complete if it proves or disproves each sentence.
A proof system $P$ is (sound and) complete with respect to an existing semantics if $P$-provability coincides with entailment in the sense of that semantics.