First, a caveat: Simpson treats the Soundness Theorem in SOSOA, but not in the way you intend it. Simpson defines (II.8.3) a model $M$ as having a truth valuation for all sentences in the language of $M$ augmented with a constant for each element of $M$. When models are defined in this way, the Soundness Theorem is provable in RCA<sub>0</sub> (II.8.8).

Now, you probably define a model in the usual manner: a set of elements together with an interpretation for each function symbol and relation symbol of the language. This is much weaker and it requires some work to go from such a traditional model to a full model in Simpson's sense. The fact that every traditional model can be extended to a full model is equivalent to ACA<sub>0</sub><sup>+</sup> (ACA<sub>0</sub> plus the assertion that every set has an &omega;-th Turing jump). Thus the Soundness Theorem (for traditional models) is provable in ACA<sub>0</sub><sup>+</sup>.

That said, ACA<sub>0</sub>' (ACA<sub>0</sub> plus the assertion that every set has a $n$-th Turing jump for every internal number $n$) proves that partial truth valuations exist: for every (internal code for a) formula $\sigma$ there is a truth valuation for all substitution instances of subformulas of $\sigma$. (ACA<sub>0</sub> only proves this for every *standard* formula $\sigma$.) So the Soundness Theorem for traditional models is actually provable in ACA<sub>0</sub>'.

In fact, the Soundness Theorem for traditional models is precisely equivalent to ACA<sub>0</sub>' over ACA<sub>0</sub>. First observe that ACA<sub>0</sub> is strong enough to prove the uniqueness (but not the existence) of partial truth valuations as described above. So it is reasonable to define the satisfaction relation for a traditional model $M$ as usual: $M \vDash \sigma$ iff there is a partial truth valuation for $\sigma$ that assigns value true to $\sigma$. The fact that this relation satisfies $M \vDash \sigma\lor\lnot\sigma$ for every $\sigma$ is then precisely equivalent to the existence of partial truth valuations for every $\sigma$. In turn, the existence of such partial truth valuations for the first-order part of a model of ACA<sub>0</sub> augmented with a predicate for the set $X$ is precisely equivalent to the existence of the $n$-th Turing jump of $X$ for every internal number $n$. Note that this reversal is a little weak since it relies on a particular definition of the satisfaction relation, but I can't think of any other reasonable definition.