  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.
