New Aspects of Reverse Mathematics

点击翻译按钮获取中文摘要

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.