逆數學

逆數學（Reverse mathematics）是數學的一個分支，大致可以看成是“從定理導向公理”而不是通常的方向(從公理到定理)。更精確一點，它試圖通過找出證明所需的充分和必要的公理來評價一批常用數學結果的邏輯有效性。

該領域由Harvey Friedman在其文章“二階算術系統及其應用（Some systems of second order arithmetic and their use）”中創立。它被Stephen G. Simpson和他的學生以及其他一些人所追隨。Simpson寫了關於該主題的參考教科書二階算數的子系統(Subsystems of Second Order Arithmetic);本條目大部分內容取自該書的簡介性質的第一章。其他參考讀物的細節參看參考。

原則

一般性

逆數學的原則如下:從一個框架語言和一個基理論—一個核心(公理)體系—開始,它可能弱到無法證明大部分我們感興趣的定理，但是它要強到足以證明一些特定的其區別和所研究的課題不相關的命題之間的等效性或者足以建立一些足夠明顯的事實(例如加法的可交換性)。在該弱的基系統之上有一個全理論，強到足以證明我們感興趣的定理，而正常的數學直覺在該理論中又不受侵害。

在基系統和全系統之間，逆數學家需求給一些公理集標上中間的強度，它們（在基系統上）互相不等價:每個系統不僅要證明這個或那個經典定理而且需要在核心體系上等價於該定理。這保證定理的邏輯強度可以被精確的衡量(至少對所選的框架語言和核心系統來說):更弱的公理系統無法證明該定理，而更強的公理系統不被該定理所蘊涵。

語言和基系統的選擇

若基系統選得太強（作為極端情況，選它為完整的策墨羅-富蘭科集合論），則逆數學沒有什麼信息：很多(全系統的,也就是說通常的數學定理)定理會成為核心系統的定理，所以他們全都等價，我們對於他們的強度一無所知。若基系統選得太弱(作為極端情況，選它為謂詞演算)，則定理間的等價關係過於細化：沒有任何東西等價除了很明顯的，同樣我們一無所知。如何選取框架語言也是一個問題：它需要不用太多翻譯便足以表達通常的數學思想，而它不應預設太強的公理否則我們會碰到和核心系統太強一樣的麻煩。

例如，雖然通常(正向的)數學使用集合論的語言，並在策墨羅-富蘭科集合論的系統中實現(這個系統，如果不加顯式的否認，被數學工作者假設為缺省基礎系統),事實上這個系統比真正所需要的強很多—這也是逆數學給我們的教訓之一。雖然逆數學特定的結果可以用集合論的框架表達，通常這不是很合適，因為這預設了太強的假定(例如任何階的集合的存在性和構造它們的一致性)。

在逆數學根據Friedman,Simpson和其他人的現在的實現中，框架語言(通常)選為二階算術，而核心理論選為遞歸理解，而全理論則為經典分析。我們接下來必須關於這些說上兩句。

二階算術

本節有點技術性，主要試圖精確描述逆數學的通常框架(也就是，二階算數子系統)。

語言

二階算數的語言是一種分為兩類的(一階謂詞演算的)語言。一些術語和變量，通常用小寫字母表示，用於指代個體/數字，它們可以視為自然數。其他變量，稱為類變量或者謂詞，並經常用大寫表示，指代個體的類/謂詞/屬性，它們可以視為自然數的集合。個體和謂詞都可以量化，所有或者存在。一個公式如果有未限定的類變量，(雖然它可能有自由類變量和確定個體變量，)稱為算式(arithmetical)。

個體術語可以用常數0，單元函數S (後續函數)和二元操作+和· (加和乘)組成。後續函數產生一個比輸入大一的自然數。關係 = (相等) 和 < (自然數的比較) 可以關聯兩個個體，而關係 ∈ (屬於) 關聯一個個體和一個類。

例如 $\forall n(n\in X\rightarrow Sn\in X)$ 是二階算數定義嚴謹的公式，它是一個算式，有一個自由類變量X和一個確定個體變量n (但是沒有確定類變量，這是算術共識的要求),而 $\exists X\forall n(n\in X\leftrightarrow n<SSSSSS0\cdot SSSSSSS0)$ 是一個定義嚴謹的公式卻不是算式，它有一個確定類變量X和一個確定個體變量n。

子系統

常用的5個子系統按照強度(stength)分別是 RCA0 (Recursive comprehension axiom); WKL0 (Weak König's lemma); ACA0 (Arithmetical comprehension axiom); ATR0 (Arithmetical transfinite recursion); Π11-CA0 (Π11 comprehension axiom);

參考

Harvey Friedman's home page （頁面存檔備份，存於互聯網檔案館）
Proceedings of the International Congress of Mathematicians (Vancouver, B.C., 1974), Vol. 1, pp. 235–242. Canad. Math. Congress, Montreal, Que., 1975.
Stephen G. Simpson's home page （頁面存檔備份，存於互聯網檔案館）
Subsystems of Second Order Arithmetic （頁面存檔備份，存於互聯網檔案館）. Perspectives in Mathematical Logic, Springer-Verlag, Berlin, 1999. ISBN 3-540-64882-8.