The study of (compact) metric spaces in second-order Reverse Mathematics (RM hereafter) is fundamentally based on separability conditions, while the latter are generally avoided in proof mining to enable the extraction of good computational data. Inspired by this observation, we study basic properties of ‘unrepresented’ compact metric spaces in Kohlenbach’s higher-order RM, i.e. we do not assume separability conditions and work with the textbook definiton of metric space. Our results are four-fold as follows, each building on the next.
• Most definitions of compactness yield third-order theorems not provable from second-order comprehension axioms. Only one very specific choice of compactness definitions yields equivalences involving the Big Five of second-order RM.
• Many basic properties of compact metric spaces inhabit the range of hyperarithmetical analysis. Until recently, few natural examples of the latter were known.
• Some basic properties of compact metric spaces, like the intermediate value theorem, are equivalent to countable choice as studied in higher-order RM.
• Some basic properties of compact metric spaces, like a continuous function has a supremum and a countable set has measure zero, imply strong axioms including Feferman’s projection principle, full second-order arithmetic, and Kleene’s quantifier $(\exists^3)$.
In conclusion, the removal of separability conditions from compact metric spaces results in rather strong theorems.