STPL  :=  soundness theorem for predicate logic
<br><br>
(see [this](http://books.google.com/books?id=Y87XKUfGlCUC&pg=PA149&lpg=PA149&dq=predicate+logic+soundness+theorem&source=bl&ots=9-5JeqFp2v&sig=4iCLsI8m6RQWQ5QV7lslsGlzWZo&hl=en&ei=EYQyTYuSOYPQsAOPqdGDBg&sa=X&oi=book_result&ct=result&resnum=2&sqi=2&ved=0CB4Q6AEwAQ#v=onepage&q=predicate%20logic%20soundness%20theorem&f=false))
<br><br><br><br><br>
When trying to figure out the strength of the STPL in reverse mathematics, I managed to convince myself of the following:
<br><br><br>
a)  [ACA0](http://en.wikipedia.org/wiki/Reverse_mathematics#Arithmetical_comprehension_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.
<br><br>
b)  ACA0 does not prove the STPL using the truth predicate as defined in (a).
<br><br>
c)  [ACA0 + [$\Delta_1^1$ induction]]  does prove the STPL as given in (b).
<br><br><br><br>
So, my questions are:
<br><br><br>
1.  Are my understandings correct?
<br><br>
2.  Does ACA0 + STPL prove $\Delta_1^1$ induction?
<br><br>
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](http://docs.google.com/viewer?a=v&q=cache:MjNqd-Egj2QJ:ests.files.wordpress.com/2010/11/neeman-luminy2010.pdf+reverse+math+reversal+%22provably+necessary%22&hl=en&gl=us&pid=bl&pg=4&srcid=ADGEESiNJkrHvNYXW17Wpj6EeANSdJWjmfSzU7C-XFqU4U8x7PWuMVib9q89UfdAxTfH7lgp10bMs0Hp6eYqYZVe8tZe2G4uvacFmbsVL9jdldCc91btak5Bxby5a1pbJBwUpjkWZ9xF&sig=AHIEtbTmRPmQs11tFQM8K3Eb1qeIgKv5Xg)?)