# Soundness Theorem in reverse mathematics

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

-
Would you need the truth predicate for arithmetic? I haven't thought carefully about what STPL would really look like in the language of second-order arithmetic, but aren't the extralogic symbols given as sets? I.e it only needs a truth predicate for logical symbols plus some extra symbols, not successor, addition, multiplication. This sounds like it ought to be simpler than Delta-1-1. –  Daniel Mehkeri Jan 16 '11 at 7:19
Excellent point re arithmetic. (fixing that now) –  Ricky Demer Jan 16 '11 at 7:20
Somewhat along the lines of Daniel's comment: some forms of STPL, at least, are provable already in RCA0 (as in II.8 of Simpson's SOSOA). –  Ed Dean Jan 16 '11 at 7:24
About the rest of Daniel's comment, a truth predicate has to be for all (codes of) first-order formulas, not just atomic formulas. –  Ricky Demer Jan 16 '11 at 7:25
I don't think STPL proves $\Delta^1_1$-induction, since it looks like STPL is provable in $ACA_0^+$. (Because $ACA_0^+$ is strong enough to comprehend the truth predicate for a model.) –  François G. Dorais Jan 16 '11 at 9:32

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