Reverse mathematics of general topology

回想一下学校，我们在那里学习数学事实或定理，比如毕达哥拉斯定理和微积分基本定理。这些事实是正确的，因为它们可以通过一连串的逻辑步骤推导出来。这是数学中的真理标准：一个数学命题被认为是真的，如果有一个合理的证据证明它是真的，它就被称为定理。因此，数学证明的目的是证明被证明的定理的绝对确定性。然而，证明是逻辑推理的链条，而链条必须从某个地方开始。每一个证明的背后都是关于数学世界如何运作的基本假设的集合，这些假设被称为公理。这些基本假设是我们研究的重点。数学在整个19世纪变得更加复杂和抽象，主要是由于代数、几何和实分析（微积分的理论基础）的巨大进步。关于某些证明的有效性的分歧出现了，对统一的数学基础的需要变得明显起来。提供这些基础的早期尝试受到矛盾的困扰，比如罗素著名的悖论。这些失败促成了20世纪初所谓的“数学基础危机”。为了应对这场危机，当时最伟大的数学家大卫·希尔伯特（David Hilbert）提出了现在被称为“希尔伯特计划”的方案。希尔伯特鼓励数学家们寻找终极公理，所有的数学命题都可以从这些公理中被证明为真或被驳斥为假；所有的证明都可以被机械地验证（现在，我们会说通过计算机）；没有矛盾的；批判地说，它可以用公理本身来证明是没有矛盾的。这样的公理将提供理想的基础，因为它们将回答任何可以想象的数学问题，而不必担心矛盾。在20世纪30年代，库尔特Gödel用他的不完备性定理震惊了数学世界，这意味着不可能有像希尔伯特所期望的那样建立所有数学的公理集合。Gödel所展示的部分内容是，合理的公理集合不能证明它们自己没有矛盾。因此，没有一个坚实的数学基础；我们永远无法确切地知道，在我们的基本假设中是否潜藏着矛盾。从Gödel、塔斯基、图灵和其他人的工作中，我们现在知道公理系统形成了一种塔。底层对应的是弱公理，可以证明的定理很少，但基础很牢固。上层对应于强大的公理，可以证明许多定理，但其基础更不稳定。在20世纪70年代，哈维·弗里德曼（Harvey Friedman）发起了一个名为“逆向数学”的项目，其目标是精确地指出，为了证明核心数学定理，人们需要爬到公理之塔的多高。这很有趣，因为通过确定需要哪些公理来证明某个定理，我们通过接受它的证明来确定我们所做的基本承诺。这样的调查也有潜在的实际好处。弱公理本质上倾向于算法，所以如果一个定理可以从弱公理中得到证明，那么有时可以从证明中提取计算信息。相反，如果一个定理需要强公理，那么这可能意味着不可能有这样的提取。在这个项目中，我们以逆向数学的方式分析拓扑（数学空间的研究）中的关键定理。迄今为止，尽管拓扑学是现代数学的核心，但这只是以一种相当零碎的方式完成的。部分问题是拓扑学是非常普遍的，而逆向数学在限制特定类型的数学对象时效果最好。我们的工作是扩展反向数学，并帮助给出一个全面的基础拓扑。

Think back to school, where we are taught mathematical facts, or theorems, such as the Pythagorean theorem and the fundamental theorem of calculus. These facts are true because they can be deduced by chains of logical steps. This is the standard of truth in mathematics: a mathematical statement is considered true and is called a theorem if there is a reasoned proof that the statement is true. Thus a mathematical proof is intended to be a demonstration of the absolute certainty of the theorem being proved. However, a proof is a chain of logical reasoning, and chains have to start somewhere. Behind every proof is a collection of basic assumptions, called axioms, about how the mathematical world works. These basic assumptions are the focus of our research.Mathematics became more intricate and more abstract throughout the 1800s, largely due to great advances in algebra, geometry, and real analysis (the theoretical basis of calculus). Disagreements concerning the validity of certain proofs arose, and the need for a unified foundations of mathematics became apparent. Early attempts to provide these foundations were plagued by contradictions, such as Russell's famous paradox. These failures precipitated the so-called "foundational crisis in mathematics" of the early 1900s. In response to the crisis, David Hilbert, the greatest mathematician of his day, proposed what is now called "Hilbert's program." Hilbert encouraged mathematicians to seek the ultimate axioms, from which all mathematical statements can be either proved true or refuted as false; for which all proofs can be verified mechanically (nowadays, we would say by a computer); which are free of contradictions; and, critically, which can be proved to be free of contradictions using the axioms themselves. Such axioms would provide the ideal foundations, as they would answer any conceivable mathematical question without fear of contradiction.In the 1930s, Kurt Gödel surprised the mathematical world with his incompleteness theorems, which imply that there can be no single collection of axioms founding all of mathematics as Hilbert desired. Part of what Gödel showed is that reasonable collections of axioms cannot prove themselves to be free of contradictions. Thus there is no solid foundation for all of mathematics; we can never know for sure that there is no contradiction lurking among our basic assumptions. From the work of Gödel, Tarski, Turing, and others, we now know that axiomatic systems form a sort of tower. The bottom levels correspond to weak axioms, where few theorems can be proved but the foundational footing is strong. The upper levels correspond to powerful axioms that can prove many theorems, but whose foundations are much shakier.In the 1970s, Harvey Friedman initiated a program called "reverse mathematics" whose goal is to pinpoint exactly how far up the axiomatic tower one needs to climb in order to prove core mathematical theorems. This is interesting because by exactly determining what axioms are required prove a certain theorem, we exactly determine the foundational commitment we make by accepting its proof. There are potential practical benefits to such an inquiry as well. Weak axioms tend to be algorithmic in nature, so if a theorem can be proved from weak axioms, then sometimes computational information can be extracted from the proof. Conversely, if a theorem requires strong axioms, then this can mean that no such extraction is possible.In this project, we analyze key theorems from topology (the study of mathematical spaces) in the style of reverse mathematics. To date, this has only been done in a fairly piecemeal fashion, despite topology being central to modern mathematics. Part of the problem is that topology is extremely general, whereas reverse mathematics works best when restricting to specific sorts of mathematical objects. We work to expand reverse mathematics and to help give a full account of the foundations of topology.