Reverse mathematics of general topology

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

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.