Reverse mathematics for the working mathematician

该项目属于EPSRC的逻辑和组合学研究领域。一长串数学逻辑学家的研究（如外尔，希尔伯特，伯奈斯，Takeuti，Feferman，弗里德曼，辛普森仅举几例）已经表明，大量的普通数学可以由相当适度的一致性强度的理论支撑。这证实了希尔伯特在他的保守性计划中所推测的，即基本结果（也就是那些可以用数论语言表达的）用抽象的、非构造性的数学证明，原则上可以用初等的方法证明。为了得到这样的结果，逻辑学家已经发展出了数学形式化的详尽理论，并表明，通过大量的复杂的技术从数学逻辑，他们是保守的各种基本理论。从普通数学中确定定理的强度的最著名的程序是反向数学（RM）。RM用于测量强度的标尺由以二阶算术语言表达的某些标准系统提供。然而，这种语言的表达能力不足以直接讨论高阶对象，如函数空间。还有其他建议，使用形式系统，其中高阶数学对象可以直接占。然而，在基本理论上保持保守性的代价是必须采用半直觉逻辑或以非集合论的方式定义函数的概念（或施加其他微妙的限制）。这个博士项目的一部分包括研究各种系统之间的联系并确定它们的强度。这需要序数分析和其他数学逻辑工具的技术。 该项目的另一个目标是找到一个正式的系统，可以很容易地学习和工作的数学家使用的反向数学。这里的一个新颖方面是对数学对象使用不同的逻辑，即对数字使用经典逻辑，但对更高类型的数学对象使用直觉逻辑。对于更高类型的对象，切换到直觉逻辑的优点是理论的逻辑强度可以被驯服，同时允许高阶语言的表达能力。直觉主义逻辑的另一个令人兴奋的方面是，它在数学中引入了公理自由的新维度。然而，对大多数数学家来说，转向直觉主义逻辑可能过于激进。因此，另一条要探索的路线旨在为更高类型的对象找到更好的公理，即使使用经典逻辑也不会产生巨大的一致性强度。

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.