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}$ 时。

0
下载
关闭预览

相关内容

知识图谱构建-关系抽取和属性抽取
深度学习自然语言处理
27+阅读 · 2020年3月1日
开年重磅——周志华团队综述归纳逻辑程序设计
计算机研究与发展
10+阅读 · 2019年1月22日
博客 | 回归类算法最全综述及逻辑回归重点讲解
AI研习社
13+阅读 · 2018年11月29日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
关系推理:基于表示学习和语义要素
计算机研究与发展
19+阅读 · 2017年8月22日
从点到线:逻辑回归到条件随机场
夕小瑶的卖萌屋
15+阅读 · 2017年7月22日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Arxiv
0+阅读 · 2月18日
Arxiv
0+阅读 · 2月9日
VIP会员
相关VIP内容
相关资讯
知识图谱构建-关系抽取和属性抽取
深度学习自然语言处理
27+阅读 · 2020年3月1日
开年重磅——周志华团队综述归纳逻辑程序设计
计算机研究与发展
10+阅读 · 2019年1月22日
博客 | 回归类算法最全综述及逻辑回归重点讲解
AI研习社
13+阅读 · 2018年11月29日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
图上的归纳表示学习
科技创新与创业
23+阅读 · 2017年11月9日
关系推理:基于表示学习和语义要素
计算机研究与发展
19+阅读 · 2017年8月22日
从点到线:逻辑回归到条件随机场
夕小瑶的卖萌屋
15+阅读 · 2017年7月22日
相关基金
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员