-
Views
-
Cite
Cite
Dag Normann, Sam Sanders, The Axiom of Choice in computability theory and Reverse Mathematics with a cameo for the Continuum Hypothesis, Journal of Logic and Computation, Volume 31, Issue 1, January 2021, Pages 297–325, https://doi.org/10.1093/logcom/exaa080
Close - Share Icon Share
Abstract
The Axiom of Choice (|${\textsf{AC}}$| for short) is the most (in)famous axiom of the usual foundations of mathematics, |${\textsf{ZFC}}$| set theory. The (non-)essential use of |${\textsf{AC}}$| in mathematics has been well-studied and thoroughly classified. Now, fragments of countable |${\textsf{AC}}$| not provable in |${\textsf{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 |${\textsf{NCC}}$|, a weak choice principle provable in |${\textsf{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 |${\textsf{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) |${\textsf{AC}}$| leads to interesting results. For instance, using Kleene’s S1-S9 computation schemes, we show that various total realisers for |${\textsf{NCC}}$| compute Kleene’s |$\exists ^{3}$|, a functional that gives rise to full second-order arithmetic, and vice versa. By contrast, partial realisers for |${\textsf{NCC}}$| should be much weaker, but establishing this conjecture remains elusive. By way of catharsis, we show that the Continuum Hypothesis (|${\textsf{CH}}$| for short) is equivalent to the existence of a countably based partial realiser for |${\textsf{NCC}}$|. The latter kind of realiser does not compute Kleene’s |$\exists ^{3}$| and is therefore strictly weaker than a total one.
