Reverse mathematics of general topology

一般拓扑的逆数学

• 批准号: EP/T031476/1
• 负责人: Paul Shafer
• 金额: $ 45.06万
• 依托单位: University of Leeds
• 依托单位国家: 英国
• 项目类别: Research Grant
• 财政年份: 2021
• 资助国家: 英国
• 起止时间: 2021 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=EP%2FT031476%2F1
• 关键词: Reverse; mathematics; general; topology

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.

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

项目成果

ORDINAL ANALYSIS OF PARTIAL COMBINATORY ALGEBRAS

部分组合代数的序分析

• DOI: 10.1017/jsl.2021.50
• 发表时间: 2021
• 期刊: The Journal of Symbolic Logic
• 作者: SHAFER P

An inside/outside Ramsey theorem and recursion theory

内/外拉姆齐定理和递归理论

• DOI: 10.1090/tran/8561
• 发表时间: 2021
• 期刊: Transactions of the American Mathematical Society
• 影响因子: 1.3
• 作者: Fiori-Carones M

ON COHESIVE POWERS OF LINEAR ORDERS

论线性秩序的凝聚力

• DOI: 10.1017/jsl.2023.14
• 发表时间: 2023
• 期刊: The Journal of Symbolic Logic
• 作者: DIMITROV R

(EXTRA)ORDINARY EQUIVALENCES WITH THE ASCENDING/DESCENDING SEQUENCE PRINCIPLE

升序/降序原则的（额外）普通等价

• DOI: 10.1017/jsl.2022.92
• 发表时间: 2022
• 期刊: The Journal of Symbolic Logic
• 作者: FIORI-CARONES M

Metric fixed point theory and partial impredicativity

• DOI: 10.1098/rsta.2022.0012
• 发表时间: 2023-05-29
• 期刊: PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES
• 影响因子: 5
• 作者: Fernandez-Duque, D.;Shafer, P.;Yokoyama, K.
• 通讯作者: Yokoyama, K.