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>'.