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 $\mathrm{RCA}_0$ (a finitistically reducible system axiomatizing recursive set comprehension only). The implication from a set existence axiom to a theorem is the usual (forward) direction of mathematics, while the implication from a theorem back to the axiom is reverse direction of reverse mathematics.
There are other uses of the term reverse mathematics, notably constructive reverse mathematics (see below).
Work on reverses mathematics has isolated five subsystems of second order arithmetic that correspond to many classical theorems. For more information see ordinal analysis.
These are in increasing order: $\mathrm{RCA}_0$, $\mathrm{WKL}_0$, $\mathrm{ACA}_0$, $\mathrm{ATR}_0$ and $\Pi^1_1{-}\mathrm{CA}_0$. The first two are finitistically reducible, but $\mathrm{WKL}_0$ introduces non-recursive sets. The system $\mathrm{ACA}_0$ has the same strength as first-order Peano arithmetic, $\mathrm{PA}$. The system $\mathrm{ATR}_0$ is predicatively reducible, while the system $\Pi^1_1{-}\mathrm{CA}_0$ corresponds to the first-order system $\mathrm{ID}_{\lt\omega}$ of finitely many generalized inductive definitions.
Constructive reverse mathematics refers to a similar program initiated by Ishihara which aims to calibrate non-constructive theorems with respect to non-constructive axioms over a constructive base theory. The non-constructive axioms he considers are
Omniscience principles, in decreasing strength: LPO (limited principle of omniscience), WLPO (weak LPO), LLPO (lesser LPO).
Variations of Markov’s Principles (MP): WMP (Weak MP), MP$^{\vee}$ (disjunctive MP).
Principles from Brouwer’s intuitionism: FAN$_\Delta$ (detachable fan principle), BD-N (boundedness principle).
Stephen G. Simpson, Subsystems of Second Order Arithmetic, 2nd edition, Cambridge University Press, 2010.
Wikipedia, Reverse mathematics
Natural examples of Reverse Mathematics outside classical analysis?, MO:q/185941
In the context of constructive mathematics:
Hajime Ishihara, Reverse Mathematics in Bishop’s Constructive Mathematics, Philosophia Scientiæ, CS 6 (2006) (doi:10.4000/philosophiascientiae.406, pdf)
Hannes Diener, Constructive Reverse Mathematics, 2018 (arXiv:1804.05495, dspace:ubsi/1306)
Takayuki Kihara, Degrees of incomputability, realizability and constructive reverse mathematics [arXiv:2002.10712]
Last revised on January 29, 2024 at 16:10:22. See the history of this page for a list of all contributions to it.