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)?)