We develop an approach to choice principles and their contrapositive bar-induction principles as extensionality schemes connecting an ''intensional'' or ''effective'' view of respectively ill-and well-foundedness properties to an ''extensional'' or ''ideal'' view of these properties. After classifying and analysing the relations between different intensional definitions of ill-foundedness and well-foundedness, we introduce, for a domain $A$, a codomain $B$ and a ''filter'' $T$ on finite approximations of functions from $A$ to $B$, a generalised form GDC$_{A,B,T}$ of the axiom of dependent choice and dually a generalised bar induction principle GBI$_{A,B,T}$ such that: - GDC$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ the general axiom of choice expressed as $\forall a\existsβR(a, b) \Rightarrow\existsα\forall a R(α,(a α(a)))$ when $T$ is a filter that derives point-wise from a relation $R$ on $A x B$ without introducing further constraints, $\bullet$ the Boolean Prime Filter Theorem / Ultrafilter Theorem if $B$ is the two-element set $\mathbb{B}$ (for a constructive definition of prime filter), $\bullet$ the axiom of dependent choice if $A = \mathbb{N}$, $\bullet$ Weak K{ö}nig's Lemma if $A = \mathbb{N}$ and $B = \mathbb{B}$ (up to weak classical reasoning) - GBI$_{A,B,T}$ intuitionistically captures the strength of $\bullet$ G{ö}del's completeness theorem in the form validity implies provability for entailment relations if $B = \mathbb{B}$, $\bullet$ bar induction when $A = \mathbb{N}$, $\bullet$ the Weak Fan Theorem when $A = \mathbb{N}$ and $B = \mathbb{B}$. Contrastingly, even though GDC$_{A,B,T}$ and GBI$_{A,B,T}$ smoothly capture several variants of choice and bar induction, some instances are inconsistent, e.g. when $A$ is $\mathbb{B}^\mathbb{N}$ and $B$ is $\mathbb{N}$.
翻译:我们提出一种方法,将选择公理及其对偶形式——条归纳原理——理解为外延性方案,它们分别将"内涵"或"有效"视角下的非良基性与良基性性质,与这些性质的"外延"或"理想"视角相连接。在对不同内涵定义下的非良基性与良基性关系进行分类分析后,我们针对定义域 $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 b R(a, b) \Rightarrow\exists\alpha\forall a R(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}$ 时。