On the Uniform Computational Content of Computability Theory
On the Uniform Computational Content of Computability Theory
复制标题
论可计算性理论的统一计算内容
DOI：
10.1007/s00224-017-9798-1
复制
发表时间：
2015
影响因子：
0.5
通讯作者：
A. Kreuzer
中科院分区：
文献类型：
--
作者：
V. Brattka;Matthew Hendtlass;A. Kreuzer
我们证明，Weihrauch格可以用来分类的统一计算内容的可计算性理论的属性，以及计算内容的定理在一个共同的设置。我们研究的属性包括对角不可计算性，超免疫性，皮亚诺算法的完全一致扩展，1-genericity，Martin-Löf随机性和凝聚力。在我们的案例研究中，我们包括的定理是Jockusch和Soare的低基定理，Kleene-Post定理和Friedberg的跳跃反演定理。事实证明，所有上述性质和可计算性理论中的许多定理，包括所有声称存在某个图灵度的定理，几乎没有统一的计算内容：它们位于二元选择的上锥（也称为LLPO）之外;我们称具有此性质的问题为无差别的。由于几乎所有的经典分析定理的计算内容已被分类是歧视性的，我们的观察可以产生一个解释，为什么定理和结果在可计算性理论通常有很少的直接后果，在其他学科，如分析。在我们的案例研究中，一个值得注意的例外是低基定理，它是判别式的。这也许就是为什么它被认为是可计算性理论中最适用的定理之一。在某些情况下，经典数学的无差别世界和有差别世界之间的桥梁可以通过一个合适的剩余运算建立，我们证明了这一点的情况下的凝聚力问题和问题的一致性完全扩展的皮亚诺算术。两者都是两个判别问题的商。
We demonstrate that the Weihrauch lattice can be used to classify the uniform computational content of computability-theoretic properties as well as the computational content of theorems in one common setting. The properties that we study include diagonal non-computability, hyperimmunity, complete consistent extensions of Peano arithmetic, 1-genericity, Martin-Löf randomness, and cohesiveness. The theorems that we include in our case study are the low basis theorem of Jockusch and Soare, the Kleene-Post theorem, and Friedberg’s jump inversion theorem. It turns out that all the aforementioned properties and many theorems in computability theory, including all theorems that claim the existence of some Turing degree, have very little uniform computational content: they are located outside of the upper cone of binary choice (also known as LLPO); we call problems with this property indiscriminative. Since practically all theorems from classical analysis whose computational content has been classified are discriminative, our observation could yield an explanation for why theorems and results in computability theory typically have very few direct consequences in other disciplines such as analysis. A notable exception in our case study is the low basis theorem which is discriminative. This is perhaps why it is considered to be one of the most applicable theorems in computability theory. In some cases a bridge between the indiscriminative world and the discriminative world of classical mathematics can be established via a suitable residual operation and we demonstrate this in the case of the cohesiveness problem and the problem of consistent complete extensions of Peano arithmetic. Both turn out to be the quotient of two discriminative problems.