---
tag: 7SQS69T17R
kind: concept
name: Reverse mathematics
msc: [03B30, 03F35]
sources:
  - url: https://en.wikipedia.org/wiki/Reverse_mathematics
same_as:
  wikidata: Q2005236
  wikipedia: Reverse mathematics
---

## Summary

Reverse mathematics is a program in mathematical logic that asks which axioms are needed to prove the theorems of ordinary mathematics.
It works in subsystems of [[second-order arithmetic|DC60FYCSPM]] over a weak base theory, and proves theorems equivalent to set existence axioms.
A striking finding is that many classical theorems are equivalent to one of five subsystems, often called the big five.

## Explanations

### L1 human

Usually one goes from axioms to theorems.
Reverse mathematics goes backwards: it starts from a theorem and finds the weakest axioms that prove it.
Often the theorem turns out to be equivalent to those axioms, so it needs exactly them.
For example, the Bolzano–Weierstrass theorem, that every bounded sequence of reals has a convergent subsequence, is equivalent to the axiom system called $\mathsf{ACA}_0$ over the base theory.