Question

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

Answer 1

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 RCA₀ (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 ACA₀⁺ (ACA₀ plus the assertion that every set has an ω-th Turing jump). Thus the Soundness Theorem (for traditional models) is provable in ACA₀⁺.

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

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