The completeness theorem - also due to Godel! - says that this always happens, at least for first-order theories:
Suppose $T$ is a first-order theory. If $\varphi$ is a sentence true in every model of $T$ then $\varphi$ is provable from $T$, and conversely. Or in symbols, $$T\models\varphi\quad\iff\quad T\vdash\varphi.$$
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.
Yes, your understanding is basically right.
In more detail:
The term "Peano arithmetic" is used variously by different communities to refer to either first or second order Peano arithmetic (I'll denote the latter by "$\mathsf{PA}_1$" and "$\mathsf{PA}_2$" respectively). Within the modern mathematical logic community, "Peano arithmetic" almost exclusively refers to $\mathsf{PA}_1$; however, in older texts and among philosophers and historians of mathematics, it often refers to $\mathsf{PA}_2$.
The theory $\mathsf{PA}_1$ is usually formulated in the language $\{0,1,+,\times,<\}$ or something similar; roughly speaking, the only crucial point is that we have both addition and multiplication (arithmetic with only addition, for example, is quite a different matter). The axioms of $\mathsf{PA}_1$ consist of:
Weakening the induction scheme to apply to only certain first-order formulas results in subtheories of $\mathsf{PA}_1$; e.g. $\mathsf{I\Sigma_{17}}$ is the fragment of $\mathsf{PA_1}$ consisting of $\mathsf{P}^-$ together with induciton for $\Sigma_{17}$ formulas.
Meanwhile, $\mathsf{PA}_2$ is usually formulated in the much smaller language $\{0,\mathsf{succ}\}$ with a very sparse set of axioms ... followed by the full second-order induction axiom. Again, there is some flexibility in the details but the power of the underlying logic is such that it ultimately doesn't matter.
(As an aside, if we build a direct analogue of $\mathsf{PA_1}$ with second-order logic replacing first-order logic in the setup of the induction scheme we get something appropriately equivalent to $\mathsf{PA}_2$; see here.)
"Second-order arithmetic" meanwhile refers to the two-sorted, first-order theory $\mathsf{Z_2}$. The two sorts are generally called "numbers" and "sets," and the axiom of extensionality (which is part of $\mathsf{Z_2}$) ensures that we can WLOG restrict attention to models whose sets sort literally consists of subsets of the numbers sort and whose elementhood relation is actual elementhood. The language of $\mathsf{Z_2}$ consists of the language of $\mathsf{PA}_1$ on the numbers sort, and the new binary relation "$\in$" connecting the numbers and sets sorts. Its axioms consist of:
$\mathsf{P}^-$ for the numbers sort,
extensionality for the sets sort, and
the full induction and comprehension schemes.
Whereas the interesting subtheories of $\mathsf{PA}_1$ essentially arise from restricting the induction scheme, $\mathsf{Z_2}$ is "two-dimensional:" we get interseting subtheories by restricting either the induction or comprehension schemes.
For further reading about $\mathsf{PA}_1$ and $\mathsf{Z_2}$, and their interesting subtheories specifically, I strongly recommend Hajek/Pudlak and Simpson respectively. See also my recommendations here and here.
Best Answer
Recall that $\textbf{RCA}_0$ can only really talk about numbers an sets of numbers. So in particular you can only talk about other objects by means of codes. The set of all finite sets of natural numbers is a third order object. This means you cannot formalize $code$ as a second order object in $\textbf{RCA}_0$ since, without $code$, the theory $\textbf{RCA}_0$ cannot refer to the set of finite sequences or sets. Usually when we say in $\textbf{RCA}_0$, or any other fragment of second order arithmetic, that a function $f$ has as domain the set of all finite sets what we actually mean is that $f$ has domain equal to the range of $code$. We can, however, take $code$ to be defined by a formula of second order arithmetic. In that case you are correct that a theory $\textbf{RCA}_0$ can prove $code$ is injective.
To be precise, lets fix some coding of the finite sets. I prefer the Ackermann interpretation in which $x\in_{Ack} y$ if the $x$-th digit of the binary representation of $y$ is $1$. This has the advantage that any number will be the code for a finite set over $\textbf{I}\Delta^0_0 +\text{exp}$. Let $Code(X,y)$ be the formula : \begin{equation} \forall n\, (n\in X \leftrightarrow n\in_{Ack} y) \end{equation} which states that $y$ codes $X$. Let $IsFin(X)$ be the formula: \begin{equation} \exists k\,\forall n\, (n\in X\rightarrow n\leq k) \end{equation} It is straight forward to show that $\textbf{RCA}$ proves that: \begin{equation} \forall X\, (IsFin(X)\rightarrow \exists! y \, Code(X,y)) \end{equation} that is $Code$ is the graph of a function from $\{X\subseteq \mathbb{N}:IsFin(X)\}\rightarrow \mathbb{N}$
\begin{equation} \forall X,Y\, \forall z\,((IsFin(X)\wedge IsFin(Y)\wedge Code(X,z)\wedge Code (Y,z))\rightarrow X=Y) \end{equation} which states informally that $Code$ is the graph of an injection. We can also show that $Code$ is bijective, that is, for any number $x$ there exists a finite set $F$ such that $x$ is the code of $F$.
Of course we cannot quantify over the finite sets without the use of coding in a theory of first order arithmetic. So in particular, as you noted, you cannot formalize the statements above.
There are a few final considerations. The first is that the technical details of how finite sets are coded as numbers is almost always the same over fragments of second order arithmetic such as $\textbf{RCA}_0$ and fragments of first order arithmetic like $\textbf{I}\Delta^0_0 + \text{exp}$. You might wonder why would one would need to code finite sets as numbers in the context of second order arithmetic if we already have finite sets. The answer is that it lowers the order of the objects one is working with. For example, to formalize Konig's lemma I need to be able to formalize what a tree is in second order arithmetic. Usually a tree is taken to be a subset of $\mathbb{N}^{<\mathbb{N}}$ which is closed under initial segments. But this is an issue since $\mathbb{N}^{<\mathbb{N}}$ is a third order object if I just have codes for pairs.