Reverse mathematics for the working mathematician

工作数学家的逆向数学

• 批准号: 2778151
• 金额: --
• 依托单位: University of Leeds
• 依托单位国家: 英国
• 项目类别: Studentship
• 财政年份: 2023
• 资助国家: 英国
• 起止时间: 2023 至 无数据
• 项目状态: 未结题
• 来源: https://gtr.ukri.org/projects?ref=studentship-2778151
• 关键词: Reverse; mathematics; working; mathematician

The project resides in the EPSRC research area of logic and combinatorics. Investigations by a long list of mathematical logicians (e.g. Weyl, Hilbert, Bernays, Takeuti, Feferman, Friedman, Simpson to name a few) have shown that large swathes of ordinary mathematics can be undergirded by theories of fairly modest consistency strength.This confirms what Hilbert surmised in his conservativity program, namely that elementary results (that is, those expressible in the language of number theory) proved in abstract,non-constructive mathematics can in principle be proved by elementary means.To obtain such results, logicians have developed elaborate theories for the formalization of mathematics, and shown, by a plethora of elaborate techniques from mathematical logic, that they are conservative over various elementary theories. The best known program for determining the strength of theorems from ordinary mathematics is reverse mathematics (RM). RM's scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic. However, this language is not expressive enough to be able to talk about higher order objects, such as function spaces, directly. There are other suggestions, using formal systems in which higher order mathematical objects can be directly accounted for. The price for maintaining conservativity over elementary theories, however, is that one has to adopt a semi-intuitionistic logic or define the concept of function in a non-set-theoretic manner (or the imposition of other subtle restrictions).One part of this PhD project consists of studying the connections between the various systems and determining their strength. This requires techniques from ordinal analysis and other tools of mathematical logic. Another goal of the project is to find a formal system for reverse mathematics that can be easily learned and used by the working mathematician. Here a novel aspect is to use different logics for mathematical objects, namely classical logic for numbers but intuitionistic logic for higher type mathematical objects. The switch to intuitionistic logic for higher type objects has the advantage that the logical strength of the theories can be tamed, while at the same time allowing for the expressiveness of higher order languages. A further exciting aspect of intuitionistic logic is that it introduces a new dimension of axiomatic freedom in mathematics. However, the switch to intuitionist logic might be too radical for most mathematicians. Thus, another route to be explored aims to find better axioms for higher type object that do not engender enormous consistency strength even when classical logic is used.

该项目属于 EPSRC 逻辑和组合学研究领域。一长串数理逻辑学家（例如 Weyl、Hilbert、Bernays、Takeuti、Feferman、Friedman、Simpson 等）的研究表明，大量普通数学可以由相当适度的一致性强度的理论来支撑。这证实了 Hilbert 在他的保守性纲领中的推测，即基本结果（即那些可以用数论语言表达的结果） 为了获得这样的结果，逻辑学家为数学形式化发展了复杂的理论，并通过大量来自数理逻辑的复杂技术表明，他们对各种基本理论是保守的。用于确定普通数学定理强度的最著名的程序是逆向数学（RM）。 RM 用于测量力量的量表由某些以二阶算术语言表示的标准系统提供。然而，这种语言的表达能力不够，无法直接谈论更高阶的对象，例如函数空间。还有其他建议，使用可以直接解释高阶数学对象的形式系统。然而，维持基本理论保守性的代价是，人们必须采用半直觉逻辑或以非集合论的方式定义函数的概念（或施加其他微妙的限制）。这个博士项目的一部分包括研究各种系统之间的联系并确定它们的强度。这需要序数分析技术和其他数理逻辑工具。 该项目的另一个目标是找到一个数学家可以轻松学习和使用的逆向数学正式系统。这里一个新颖的方面是对数学对象使用不同的逻辑，即对数字使用经典逻辑，而对更高类型的数学对象使用直觉逻辑。对于更高类型的对象，转向直觉逻辑的优点是可以驯服理论的逻辑强度，同时允许更高阶语言的表达能力。直觉逻辑的另一个令人兴奋的方面是它引入了数学中公理自由的新维度。然而，对于大多数数学家来说，转向直觉主义逻辑可能过于激进。因此，要探索的另一条路线旨在为更高类型的对象找到更好的公理，即使使用经典逻辑，这些公理也不会产生巨大的一致性强度。