逆数学とは、数学の定理の証明に必要な公理を決定しようとする数理論理学のプログラムである。簡単に言えば、通常の数学が公理から定理を導くのとは逆に、「定理から公理を証明する」手法を用いることが特徴である。「選択公理とツォルンの補題はZF上で同値である」、というような集合論の古典的定理は、逆数学プログラムの予兆となるものだった。しかし、実際の逆数学では主に、集合論の公理ではなく、通常の数学の定理を研究するのを目的とする。
逆数学は大抵の場合、2階算術について実行され、定理が構成的解析と証明論に動機付けられた2階算術の部分体系のうち、どれに対応するのかを研究する。 2階算術を使うことで、再帰理論からの多くの技術も利用できる。実際、逆数学の結果の多くは、計算可能性解析の結果を反映している。
逆数学は、Harvey Friedman (1975, 1976)によってはじめて言及された。基本文献は(Simpson 2009)を参照。
逆数学は、フレームとなる言語と基本的な公理からはじめる。例えば、“すべての実数の有界な列は上限をもつ”という定理の研究には、実数と実数の列を定義する公理が必要となる。
基本体系において証明できない定理からはじめて、定理を証明するのに必要な(基本体系よりも強い)公理を決定することを目標とする。定理
T
T\,とそれを証明可能な場合の体系
S
S\,との関係を示す2つの証明がある。1つ目は、
S
S\,から
T
T\,が証明可能であることの証明である。このとき普通の数学の定理は体系
S
S\,で成り立つ。2つ目は*逆方向*、 すなわち
T
T\,が
S
S\,と同値であることであることの基本体系における証明である。 逆方向の証明ができれば、
S
S\,より弱い体系
S
′
S^{\prime }\,であって
T
T\,を証明できるようなものは存在しないことが分かる。
逆数学は2階算術の部分体系において研究されることが多い。その場合、数学的対象を自然数と自然数の集合によって形式化しなければならない。例えば、自然数のペアを1つの自然数として表現することができ、自然数のペアによって有理数を表現する。有理数の集合（これは結局、自然数の集合として表現される）によって有理数の列を表現し、有理数の列のうちコーシー列であるようなものによって実数を表現することができる。逆数学の研究においては、弱い部分体系であって数学的対象を形式化できる程度には強い体系を基本体系として用いる。
逆数学が集合論ではなく2階算術を用いるのは、弱い部分体系であって数学的対象を形式化できる程度には強い体系を2階算術では自然に定義することができるからである。
2階算術を使う場合、数学の定理を制限しなければならない。例えば、2階算術では一般のベクトル空間は表現できない。そのため"すべてのベクトル空間は基底をもつ"という一般的な原理は表現できないが、"すべての可算なベクトル空間は基底をもつ"という原理は表現することができる。同様に、代数の定理の対象は可算な群や環や体についてのものになる。また、距離空間を対象とする解析や位相の定理は、実数を有理数のコーシー列によって表現したのと同様の手法により、可分な距離空間について考察することができる。 なお、定理を可算なものに制限した場合、本来の定理とその強さが全く異なる場合がある。例えば、"すべての体は代数的閉体をもつ"はZF集合論では証明できないが、"すべての可算な体は代数的閉体をもつ"と制限すれば、非常に弱い弱い形式体系である
RCA
0
{\mbox{RCA}}_{0}\,でも証明することができる。
RCA
0
{\mbox{RCA}}_{0}\,は、「ロビンソン算術の公理」＋「
Σ
1
0
\Sigma _{1}^{0}\,論理式に対する帰納法の公理」＋「
Δ
1
0
\Delta _{1}^{0}\,論理式に対する内包公理」からなる部分体系である。
RCA
0
{\mbox{RCA}}_{0}\,は逆数学で最も多用される体系である。
RCA
0
{\mbox{RCA}}_{0}\,は"再帰的内包公理"と呼ばれ、"再帰的"とは"計算可能"を意味している。この名称は
RCA
0
{\mbox{RCA}}_{0}\,が"計算可能性数学"に類似しているからである。
RCA
0
{\mbox{RCA}}_{0}\,で存在が証明可能な自然数の集合は計算可能である、よって計算不可能な集合の存在は
RCA
0
{\mbox{RCA}}_{0}\,で証明できない。
RCA
0
{\mbox{RCA}}_{0}\,はBig Fiveで最弱だが、古典的数学の対象を形式化できる。また、以下の定理が証明可能である。
自然数全体、整数全体、有理数全体の成す集合の基本性質(例えば、有理数全体が順序体を成すこと)。
実数全体の成す集合の基本性質(実数全体がアルキメデス順序体であること、長さが0に近付く任意の包含閉区間列の交叉が1点のみからなること、実数は非可算であること)。
完備可分距離空間におけるベールの範疇定理。
実連続関数における中間値の定理。
可分バナッハ空間における連続線形演算子の列に関するバナッハ–シュタインハウスの定理。
弱いゲーデルの完全性定理。
可算な体での代数的閉体の存在(一意性は除く)。
可算な順序体の実閉体の存在と一意性。
RCA
0
{\mbox{RCA}}_{0}\,の1階部分は、
I
Σ
1
{\mbox{I}}\Sigma _{1}\,（ペアノ算術の帰納法を
Σ
1
\Sigma _{1}\,論理式に制限した体系）と一致する。
位相幾何学において、ジョルダン曲線定理（ジョルダンきょくせん-ていり、Jordan curve theorem）あるいはジョルダンの閉曲線定理（へいきょくせんていり）とは、平面に置かれた自己交差を持たないどんな閉曲線（輪っか）も平面を「内側」と「外側」に分けるということを述べた定理。
