Classical reverse mathematics is a research programme, started over thirty years ago by Harvey Friedman (Friedman 1975), in which the aim is to place the theorems of large parts (perhaps all?) of mathematics into a number of equivalence classes, the theorems in any given class being equivalent to some natural set-existence principle. Currently, as presented in the compendious text by Simpson (Simpson 1999), five such equivalence classes are used, whose representing set-existence principles can be placed in increasing order of logical complexity. For example, it is known that both the Bolzano-Weierstrass theorem on the extraction of convergent subsequences and the Ascoli-Arzelà theorem on compact subsets of function spaces are equivalent to the second principle in that hierarchy (Simpson 1984), Theorem 4.2).