On some subtheories of strong dependent choice

Abstract

In this paper, we give characterizations of the set of ${\Pi }_e^1$-consequences, ${\Sigma }_e^1$-consequences and $\mathsf{B}({\Pi }_e^1)$-consequences of the axiomatic system of the strong dependent choice for ${\Sigma }_i^1$ formulas ${\Sigma }_i^1$-${\mathsf{SDC}}_0$ for $i>0$ and $e<i+2$. Here, $\mathsf{B}(\Gamma )$ denotes the set generated by $\wedge ,\vee ,\neg$ starting from $\Gamma$.