On some subtheories of strong dependent choice

TL;DR

This paper characterizes the logical consequences of strong dependent choice axioms for certain classes of formulas, providing a detailed analysis of their set-theoretic implications.

Contribution

It offers new characterizations of the consequences of strong dependent choice for various classes of formulas, advancing understanding of their logical strength.

Findings

Characterizations of $ ext{Pi}^1_e$-consequences

Characterizations of $ ext{Sigma}^1_e$-consequences

Analysis of $ ext{B}( ext{Pi}^1_e)$-consequences

Abstract

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