Reverse mathematics refers mainly to a program introduced by Harvey Friedman and Stephen Simpson, which aims to establish for many theorems of classical analysis exactly which set existence principles they rely on. They consider the formalization of analysis based on Polish spaces in the language of second order arithmetic (hence the need to focus on separable spaces). One then tries to show that various theorems are equivalent to a set existence axiom relative to a weak base theory, usually (a.