Reverse mathematics has its origins in Harvey Friedman's 1974 address to the International Congress of Mathematicians. In it Friedman asked two fundamental questions: "What are the proper axioms to use in carrying out proofs of particular theorems, or bodies of theorems, in mathematics?" and "What are those formal systems which isolate the essential properties needed to prove them?" Reverse mathematics was developed as an attempt to answer these questions, and since 1974 many logicians (especially Friedman and Stephen Simpson) have contributed to this project.

The goal in reverse mathematics is to find the minimal collection S of set theoretic axioms which suffices to prove a given theorem T. Because Zermelo-Frankel set theory is too powerful to provide this type of delicate analysis, second order arithmetic is used as the axiomatization of set theory. The formal language of second order arithmetic contains the symbols +, ·, <, 0, 1, ∈, and =, as well as two...