 In the 1970s, Harvey Friedman initiated a research programme of reverse mathematics, aiming to classify mathematical theorems according to their equivalence to one of a small number of set-theoretic principles (Friedman 1975). This classification reveals interesting, sometimes remarkable, differences in proof-theoretic complexity. For example, although the Ascoli–Arzelà theorem is used in the standard proof of Peano’s existence theorem for solutions of ordinary differential equations (Hurewicz [1958], page 10), a reverse-mathematical analysis shows that the former is equivalent to a strictly stronger set-theoretic principle than the one equivalent to Peano’s theorem (Simpson [1984], Theorems 3.9 and 4.2). The standard treatise on classical reverse mathematics is (Simpson [1999/2009]). 