Skip to main content
addendum
Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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.

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

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.

Source Link
François G. Dorais
  • 44.4k
  • 6
  • 150
  • 233

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