EFFECTIVE CHOICE AND BOUNDEDNESS PRINCIPLES IN COMPUTABLE ANALYSIS
EFFECTIVE CHOICE AND BOUNDEDNESS PRINCIPLES IN COMPUTABLE ANALYSIS
复制标题
DOI：
10.2178/bsl/1294186663
复制
发表时间：
2011-03-01
影响因子：
0.6
通讯作者：
Gherardi, Guido
中科院分区：
文献类型：
--
作者：
Brattka, Vasco;Gherardi, Guido
在本文中，我们研究了一种新的方法来分类数学定理根据其计算内容。基本上，我们问的问题是，哪些定理可以连续地或可计算地相互转换？为了这个目的，定理被认为是通过其实现，这是与某些输入和输出数据的操作。Weihrauch约简及其所导出的偏序度结构是表达这些运算之间连续或可计算关系的技术工具，我们确定了作为Weihrauch度基石的若干选择原则，如余有限选择、离散选择、区间选择、紧选择和闭选择，并证明了分析学中的某些核心定理可以自然地归类于这种结构中.特别地，我们研究了诸如介值定理、Baire范畴定理、Banach逆映射定理、闭图定理和一致有界性定理等定理。我们还探讨如何现有的分类的哈恩-巴拿赫定理和弱柯尼希引理适合这张照片。来自构造性数学的众所周知的全知原则，如LPO和LLPO，也可以自然地被认为是Weihrauch度，它们在我们的分类中起着重要的作用。在此基础上，我们比较我们的分类与现有的分类在建设性和逆向数学的结果，我们声称，在一定意义上，我们的分类更精细，并揭示了一些新的光各自的定理的计算内容。我们的分类方案不需要任何特定的逻辑框架或公理设置，但它可以在经典数学的框架下使用拓扑学，可计算性理论和可计算分析的工具进行。我们开发了一些分离技术的基础上，一个新的并行化原则，在一定的不变性性质的Weihrauch约简，低基定理的Jockusch和Soare和Baire类定理。最后，我们提出了一些元定理，允许推导出上界的分类Weihrauch度的许多定理，我们讨论了布劳威尔不动点定理作为一个例子。
In this paper we study a new approach to classify mathematical theorems according to their computational content. Basically, we are asking the question which theorems can be continuously or computably transferred into each other? For this purpose theorems are considered via their realizers which are operations with certain input and output data. The technical tool to express continuous or computable relations between such operations is Weihrauch reducibility and the partially ordered degree structure induced by it. We have identified certain choice principles such as co-finite choice, discrete choice, interval choice, compact choice and closed choice, which are cornerstones among Weihrauch degrees and it turns out that certain core theorems in analysis can be classified naturally in this structure. In particular, we study theorems such as the Intermediate Value Theorem, the Baire Category Theorem, the Banach Inverse Mapping Theorem, the Closed Graph Theorem and the Uniform Boundedness Theorem. We also explore how existing classifications of the Hahn-Banach Theorem and Weak Konig's Lemma fit into this picture. Well-known omniscience principles from constructive mathematics such as LPO and LLPO can also naturally be considered as Weihrauch degrees and they play an important role in our classification. Based on this we compare the results of our classification with existing classifications in constructive and reverse mathematics and we claim that in a certain sense our classification is finer and sheds some new light on the computational content of the respective theorems. Our classification scheme does not require any particular logical framework or axiomatic setting, but it can be carried out in the framework of classical mathematics using tools of topology, computability theory and computable analysis. We develop a number of separation techniques based on a new parallelization principle, on certain invariance properties of Weihrauch reducibility, on the Low Basis Theorem of Jockusch and Soare and based on the Baire Category Theorem. Finally, we present a number of metatheorems that allow to derive upper bounds for the classification of the Weihrauch degree of many theorems and we discuss the Brouwer Fixed Point Theorem as an example.