The Axiom of Choice in Computability Theory and Reverse Mathematics, with a cameo for the Continuum Hypothesis

TL;DR

This paper explores the role of the Axiom of Choice in computability and reverse mathematics, showing how weak choice principles relate to computational functionals and the continuum hypothesis.

Contribution

It demonstrates that weak choice principles like NCC suffice for many reverse mathematics results and analyzes the computational strength of their realisers, linking to the continuum hypothesis.

Findings

Total realisers for NCC compute Kleene's ∃^3

Partial realisers for NCC are weaker and do not compute ∃^3

The continuum hypothesis is equivalent to the existence of a countably based partial realiser for NCC

Abstract

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.