论选择公理与杆归纳原理的逻辑结构

我们发展了一种将选择原理及其对偶的杆归纳原理视为外延性方案的方法，这些方案将分别关于良基性与非良基性性质的“内涵”或“有效”观点连接到这些性质的“外延”或“理想”观点。在分类并分析了非良基性与良基性的不同内涵定义之间的关系后，我们针对域$A$、陪域$B$以及函数从$A$到$B$的有限逼近上的“过滤器”$T$，引入了依赖选择公理的广义形式GDC$_{A,B,T}$以及对偶的广义杆归纳原理GBI$_{A,B,T}$，使得：— GDC$_{A,B,T}$直觉地捕获了以下强度：$\bullet$ 当$T$是从$A \times B$上关系$R$逐点导出且不引入进一步约束的过滤器时，表达为$\forall a\exists\beta R(a, b) \Rightarrow\exists\alpha\forall a R(\alpha,(a \alpha (a)))$的一般选择公理；$\bullet$ 若$B$为二元素集合$\mathbb{B}$（对素过滤器的构造性定义），则捕获布尔素过滤器定理/超过滤器定理；$\bullet$ 若$A = \mathbb{N}$，则捕获依赖选择公理；$\bullet$ 若$A = \mathbb{N}$且$B = \mathbb{B}$（直至弱经典推理），则捕获弱柯尼希引理；— GBI$_{A,B,T}$直觉地捕获了以下强度：$\bullet$ 若$B = \mathbb{B}$，则捕获哥德尔完备性定理（以有效性蕴含可证性之于衍推关系的形式）；$\bullet$ 若$A = \mathbb{N}$，则捕获杆归纳；$\bullet$ 若$A = \mathbb{N}$且$B = \mathbb{B}$，则捕获弱扇定理。相反，尽管GDC$_{A,B,T}$与GBI$_{A,B,T}$平滑地捕获了选择与杆归纳的若干变体，某些实例是不一致的，例如当$A$为$\mathbb{B}^\mathbb{N}$且$B$为$\mathbb{N}$时。