Banach’s theorem in higher-order reverse mathematics

Article type: Research Article

Authors: Hirst, Jeffry L.^{a; *} | Mummert, Carl^b

Affiliations: [a] Department of Mathematical Sciences, Appalachian State University, Boone, NC, USA | [b] Department of Computer and Information Technology, Marshall University, Huntington, WV, USA

Correspondence: [*] Corresponding author. hirstjl@appstate.edu.

Abstract: In this paper, methods of second-order and higher-order reverse mathematics are applied to versions of a theorem of Banach that extends the Schröder–Bernstein theorem. Some additional results address statements in higher-order arithmetic formalizing the uncountability of the power set of the natural numbers. In general, the formalizations of higher-order principles here have a Skolemized form asserting the existence of functionals that solve problems uniformly. This facilitates proofs of reversals in axiom systems with restricted choice.

Keywords: Reverse mathematics, Weihrauch reducibility, bijection, metric spaces

DOI: 10.3233/COM-230453

Journal: Computability, vol. 12, no. 3, pp. 203-225, 2023