可计算性理论和逆向数学中的选择公理，以及连续统假设的客串
The Axiom of Choice in Computability Theory and Reverse Mathematics, with a cameo for the Continuum Hypothesis
摘要：
选择选择公理（简称AC）是通常的数学基础ZFC集合论中最著名的公理。AC在数学中的（非）必要使用已经得到了很好的研究和彻底的分类。现在，在ZF中不可证明的可数AC片段最近被用于Kohlenbach的高阶逆向数学中，以获得紧密相关的紧性和局部全局原理之间的等价性。我们继续这项研究，并表明，NCC，弱选择原则证明在ZF和更弱的系统，足以满足许多这些结果。鉴于逆向数学和可计算性理论之间的密切联系，我们还研究了NCC的实现者，即从其他数据中产生选择函数的泛函。我们的傲慢承担迄今欠发达的研究（选择函数从）AC的计算特性导致有趣的结果。例如，使用Kleene的S1-S9计算方案，我们表明，各种总实现NCC计算Kleene的$\exists^3$，一个功能，产生完整的二阶算术，反之亦然。相比之下，NCC的部分实现者应该要弱得多，但建立这个猜想仍然是难以捉摸的。通过宣泄，我们证明了连续统假设（简称CH）等价于NCC的可数基部分实现者的存在性。后一种实现器不计算Kleene的$\exists^3$，因此严格弱于全实现器。
英文摘要：
The Axiom of Choice (AC for short) is the most (in)famous axiom of the usual foundations of mathematics, ZFC set theory. The (non-)essential use of AC in mathematics has been well-studied and thoroughly classified. Now, fragments of countable AC not provable in ZF have recently been used in Kohlenbach's higher-order Reverse Mathematics to obtain equivalences between closely related compactness and local-global principles. We continue this study and show that NCC, a weak choice principle provable in ZF and much weaker systems, suffices for many of these results. In light of the intimate connection between Reverse Mathematics and computability theory, we also study realisers for NCC, i.e. functionals that produce the choice functions claimed to exist by the latter from the other data. Our hubris of undertaking the hitherto underdeveloped study of the computational properties of (choice functions from) AC leads to interesting results. For instance, using Kleene's S1-S9 computation schemes, we show that various total realisers for NCC compute Kleene's $\exists^3$, a functional that gives rise to full second-order arithmetic, and vice versa. By contrast, partial realisers for NCC should be much weaker, but establishing this conjecture remains elusive. By way of catharsis, we show that the Continuum Hypothesis (CH for short) is equivalent to the existence of a countably based partial realiser for NCC. The latter kind of realiser does not compute Kleene's $\exists^3$ and is therefore strictly weaker than a total one.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
