STPL := soundness theorem for predicate logic
  
  

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

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

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 first-order structures.
  
  

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

(EDIT: Based on François's answer, I now believe that I was wrong about (a). First, the two formulas I was thinking of aren't provably equivalent; second, the $\Sigma\_1^1$ formula, which comes closer to working, does not provably satisfy ($\operatorname{True}(\lnot p) \leftrightarrow \lnot \operatorname{True}(p))$).
  
  
  
  

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](http://docs.google.com/viewer?a=v&q=cache%3aMjNqd-Egj2QJ%3aests.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)?)



Soundness Theorem in reverse mathematics
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 RCA0 (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 ACA0+ (ACA0 plus the assertion that every set has an ω-th Turing jump). Thus the Soundness Theorem (for traditional models) is provable in ACA0+.


That said, ACA0' (ACA0 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$. (ACA0 only proves this for every *standard* formula $\sigma$.) So the Soundness Theorem for traditional models is actually provable in ACA0'.


In fact, the Soundness Theorem for traditional models is precisely equivalent to ACA0' over ACA0. First observe that ACA0 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 ACA0 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.


