STPL := soundness theorem for predicate logic

(see this)




When trying to figure out the strength of the STPL in reverse mathematics, I managed to convince myself of the following:


a) ACA0 has a (provably) $\Delta_1^1$ pair of formulas, which it proves enough about to consider them as defining in it the truth predicate for arithmetical formulas.

b) ACA0 does not prove the STPL using the truth predicate as defined in (a).

c) [ACA0 + [$\Delta_1^1$ induction]] does prove the STPL as given in (b).



So, my questions are:

1. Are my understandings correct?
   
   
2. Does ACA0 + STPL prove $\Delta_1^1$ induction?
   
   
3. Is anything else known about the positions of STPL and $\Delta_1^1$ induction in the reverse mathematics hierarchy? (For example, where would they go on the list on page 4 here?)