Countable sets versus sets that are countable in Reverse Mathematics

TL;DR

This paper explores how the formulation of countability affects the strength of theorems in Reverse Mathematics, revealing that using 'countable set' instead of 'sequence' often weakens their logical strength.

Contribution

It investigates the impact of different definitions of 'countable' on the strength of classical theorems within higher-order Reverse Mathematics.

Findings

Replacing 'sequence' with 'countable set' reduces the theorems' logical strength.

'Countable set' formulations lead to 'tamer' theorems in the Reverse Mathematics zoo.

The choice of definition of 'countable' influences the strength of theorems involving uncountability.

Abstract

The program Reverse Mathematics (RM for short) seeks to identify the axioms necessary to prove theorems of ordinary mathematics, usually working in the language of second-order arithmetic $L_{2}$. A major theme in RM is therefore the study of structures that are countable or can be approximated by countable sets. Now, countable sets are represented by sequences here, because the usual higher-order definition of `countable set'cannot be expressed in $L_{2}$. Working in Kohlenbach's higher-order RM, we investigate various central theorems, e.g. those due to K\"onig, Ramsey, Bolzano, Weierstrass, and Borel, in their (often original) formulation involving the usual definition(s) of `countable set' instead of `sequence'. This study turns out to be closely related to the logical properties of the uncountably of $\mathbb{R}$, recently developed by the author and Dag Normann. Now, `being countable' can be expressed by the existence of an injection to $\mathbb{N}$ (Kunen) or the existence of a bijection to $\mathbb{N}$ (Hrbacek-Jech). The former (and not the latter) choice yields `explosive' theorems, i.e. relatively weak statements that become much stronger when combined with discontinuous functionals, even up to $\Pi_2^1$-CA$_0$. Nonetheless, replacing `sequence' by `countable set' seriously reduces the first-order strength of these theorems, whatever the notion of `set' used. Finally, we obtain `splittings' involving e.g. lemmas by K\"onig and theorems from the RM zoo, showing that the latter are `a lot more tame' when formulated with countable sets.