New Aspects of Reverse Mathematics

数学论证从一系列被称为“公理”的假设出发，通过逻辑推理推导出被称为“定理”的结论。这些从公理推导出的定理叫做“证明”。例如，著名的毕达哥拉斯定理可以从几何的基本公理中得到证明。给出一个定理的证明，人们可能会问，这些公理的使用效率有多高。也许有些公理与我们的论点无关。也许有些公理是矫枉过正，同样的定理的另一个证明可以从更温和的假设开始。或者，每一条公理都被充分利用了，少一条公理就不可能逃脱惩罚。“逆向数学”是一个数学逻辑程序，旨在解决这类问题。给定一个数学定理，证明它所需要的精确公理是什么？逆向数学是由H.弗里德曼在20世纪70年代提出的，由S。辛普森，今天是一个重大的研究举措，在十字路口的可计算性理论和证明理论。其基本思想如下。假设你想证明某个强公理A在某个定理T的证明中是必要的。要做到这一点，将定理T视为一个新的公理，并尝试仅使用T和一些允许基本数学操作的弱公理来证明公理A为定理。如果可以做到这一点，这意味着定理T蕴涵公理A，这意味着公理A是获得定理T所必需的。这种从定理而不是从公理中证明公理的方法被称为“逆向”，这也是逆向数学的名称。逆向数学中的大部分工作都是从组合学、代数和完全可分度量空间的分析中分析定理。该项目将程序推向工作较少的领域，例如更一般空间的分析和拓扑。一个焦点是度量化定理，它建立了数学空间可以通过距离概念描述的条件。逆向数学提供了一个正式的框架来讨论数学定理的复杂性，定理如何相互关联，以及证明什么样的定理需要什么样的论证。逆向数学程序也对那些从事形式化数学和证明助手的人有潜在的兴趣。逆向数学的部分研究涉及用普通语言产生“半形式”证明，但其中一个保持仔细跟踪的逻辑系统，其中一个正在工作。这是普通的非正式教科书证明和完全计算机化的证明之间的一个很好的中间点。

Mathematical arguments start from a collection of assumptions called 'axioms' and reason logically to deduce conclusions that are called 'theorems.' These deductions of theorems from axioms are called 'proofs.' For example, the famous Pythagorean theorem can be proved from basic axioms about geometry. Given a proof of a theorem, one may then ask how efficiently the axioms are being used. Maybe some of the axioms are extraneous to the argument at hand. Maybe some of the axioms are overkill, and another proof of the same theorem can be given starting from much milder assumptions. Or maybe every axiom is used to its full extent, and it is impossible to get away with less. 'Reverse mathematics' is a program in mathematical logic designed to address this sort of question. Given a mathematical theorem, what are the precise axioms required to prove it? Reverse mathematics was introduced by H. Friedman in the 1970s, greatly expanded by S. Simpson, and today is a major research initiative at the crossroads of computability theory and proof theory. The basic idea works as follows. Suppose you want to show that a certain strong axiom A is necessary in the proof of some theorem T. To do that, treat theorem T as a new axiom and try to prove axiom A as a theorem using only T and some weak axioms that allow for basic mathematical manipulations. If this can be done, it means that theorem T implies axiom A, which means that axiom A is necessary to obtain theorem T in the first place. Such proofs of axioms from theorems rather than theorems from axioms are called 'reversals' and are what give reverse mathematics its name.Much of the work in reverse mathematics analyzes theorems from combinatorics, from algebra, and from analysis on complete separable metric spaces. This project pushes the program into areas where less work has been done, such as analysis and topology on more general spaces. One focus is metrization theorems, which establish conditions under which mathematical spaces can be described via notions of distance. Reverse mathematics gives a formal framework for discussing the complexities of mathematical theorems, how theorems relate to each other, and what sort of arguments are necessary to prove what sort of theorems. The reverse mathematics program is also of potential interest to those working on formalized mathematics and proof assistants. Part of research in reverse mathematics involves producing 'semi-formal' proofs in ordinary language, but where one keeps careful track of the logical system in which one is working. This is a good intermediate point between ordinary informal textbook proofs and fully computerized proofs.