Editing Proof theory (section)

==Reverse mathematics==
{{Main|Reverse mathematics}}

Reverse mathematics is a program in [[mathematical logic]] that seeks to determine which axioms are required to prove theorems of mathematics.{{sfn|Simpson|2010}} The field was founded by [[Harvey Friedman (mathematician)|Harvey Friedman]]. Its defining method can be described as "going backwards from the [[theorem]]s to the [[axiom]]s", in contrast to the ordinary mathematical practice of deriving theorems from axioms. The reverse mathematics program was foreshadowed by results in set theory such as the classical theorem that the [[axiom of choice]] and [[Zorn's lemma]] are equivalent over [[ZF set theory]]. The goal of reverse mathematics, however, is to study possible axioms of ordinary theorems of mathematics rather than possible axioms for set theory.

In reverse mathematics, one starts with a framework language and a base theory—a core axiom system—that is too weak to prove most of the theorems one might be interested in, but still powerful enough to develop the definitions necessary to state these theorems.  For example, to study the theorem "Every bounded sequence of [[real number]]s has a [[supremum]]" it is necessary to use a base system that can speak of real numbers and sequences of real numbers.

For each theorem that can be stated in the base system but is not provable in the base system, the goal is to determine the particular axiom system (stronger than the base system) that is necessary to prove that theorem. To show that a system ''S'' is required to prove a theorem ''T'', two proofs are required. The first proof shows ''T'' is provable from ''S''; this is an ordinary mathematical proof along with a justification that it can be carried out in the system ''S''. The second proof, known as a '''reversal''', shows that ''T'' itself implies ''S''; this proof is carried out in the base system. The reversal establishes that no axiom system ''S&prime;'' that extends the base system can be weaker than ''S'' while still proving&nbsp;''T''.

One striking phenomenon in reverse mathematics is the robustness of the ''Big Five'' axiom systems. In order of increasing strength, these systems are named by the initialisms RCA<sub>0</sub>, WKL<sub>0</sub>, ACA<sub>0</sub>, ATR<sub>0</sub>, and Π{{su|p=1|b=1}}-CA<sub>0</sub>. Nearly every theorem of ordinary mathematics that has been reverse mathematically analyzed has been proven equivalent to one of these five systems. Much recent research has focused on combinatorial principles that do not fit neatly into this framework, like RT{{su|p=2|b=2}} (Ramsey's theorem for pairs).

Research in reverse mathematics often incorporates methods and techniques from [[recursion theory]] as well as proof theory.