Proof theory, higher order theories of reverse mathematics, and semi-intuitionism

该项目属于EPSRC逻辑学和组合学研究领域。逆向数学是研究数学定理的逻辑强度的一个研究领域。传统上，测量强度的尺度是由某些用二阶算术语言表述的标准体系提供的。粗略地说，一个数学定理M具有强度T （T是标准尺度上的理论之一），如果T证明M，而没有一个较弱的理论证明M。然而，理论的标准尺度是基于二阶算术的相当贫乏的语言，其本体仅限于自然数和自然数的集合，因此没有足够的表达能力来谈论高阶集。在这个项目中，目的是利用高阶理论的尺度发展逆向数学。另一个新颖的方面是对数学对象使用不同逻辑的理论，即对数字使用经典逻辑，而对高等类型的数学对象使用直觉逻辑。对高级类型对象切换到直觉逻辑的好处是，理论的逻辑强度可以被驯服，同时允许高级类型语言的表达性。直觉主义逻辑的另一个令人兴奋的方面是，它在数学中引入了公理自由的一个新维度，在这个维度中，经典逻辑不可能实现的新原理，可以用于数学定理的证明。该项目需要研究更高类型系统的证明理论强度，使用从序数分析和功能解释的技术。该项目的另一个重要部分将是在半直觉理论中发展数学，这一理论从未以系统的方式进行过。

The project resides in the EPSRC research area of logic and combinatorics. Reverse mathematics is a research area concerned with the logical strength of mathematical theorems.Traditionally, a scale for measuring strength is furnished by certain standard systems couched in the language of second order arithmetic.Roughly, a mathematical theorem M has strength T (with T be a one of the theories on the standard scale) if T proves M whereas none of the weaker theories proves M. The standard scale of theories, however, is based on the rather impoverished language of second order arithmetic whose ontology is restricted to natural numbers and sets of naturalnumbers, and therefore is not expressive enough to be able to talk about higher order sets. In this project the aim is to develop reverse mathematics using a scale of higher order theories.A novel aspect is also to use theories that 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 type languages. A further exciting aspect of intuitionistic logic is that it introduces a new dimension of axiomatic freedom in mathematics in that new principles, which are impossible with classical logic, can be employed in proofs of mathematical theorems.The project requires the study of the proof-theoretic strength of higher-type systems, using techniques from ordinal analysis and functional interpretation. Another important part of the project will be the development of mathematics in semi-intuitionistic theories which has never been carried out in a systematic way.