Return to 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 is closer to being correct, 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?)

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

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



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

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 is closer to being correct, 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?)

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 arithmetical formulas.

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



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

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



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