Banach's theorem in higher order reverse mathematics

TL;DR

This paper explores the application of higher order reverse mathematics to Banach's theorem extending Schroeder-Bernstein, and investigates uncountability in higher order arithmetic, focusing on formalizations involving functionals and restricted choice.

Contribution

It introduces new formalizations of higher order principles with Skolemized functionals, enabling reversals in systems with limited choice, and extends Banach's theorem in the reverse mathematics framework.

Findings

Formalizations of higher order principles with functionals

Reversal proofs in systems with restricted choice

Extensions of Banach's theorem in higher order reverse mathematics

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 Schroeder-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.