反推数学及相关可计算性理论问题

Reverse mathematics is a new area of mathematical logic, which has connections with the four classical branches of mathematical logic and ordinary mathematics as well. The aim of reverse mathematics is to study proof theoretic strength of theorems in ordinary mathematics by formulating ordinary mathematics in terms of second order arithmetic. In recent decades, reverse mathematics has enjoyed rapid development, mainly because it inspires computability theorists. In this project, we plan to investigate the most active topic in reverse mathematics - - the reverse mathematics of Ramsey theory, in particular combinatorial principles in Ramsey theory concerning n-ary relations for n > 2. We also plan to study a strong form of Ramsey's theorem - - Hindman's theorem. Recently there have been some surprisingly successful applications of non-standard models of arithmetic in reverse mathematics. We shall study the relation between Ramsey theory and non-standard models and try to calibrate first order theories of second order propositions. Besides, we plan to consider computability problems related to reverse mathematics, in particular, the interaction between reverse mathematics and another emerging area - - algorithmic randomness. We shall search for uniform technical approaches for solving problems in reverse mathematics.

反推数学是数理逻辑中一个沟通各个传统分支且联系经典数学的新兴领域，其目标是通过用二阶算术形式化经典数学理论，研究经典数学定理的证明论强弱。最近二十多年来，反推数学由于可计算性理论学界的重视和推动蓬勃发展。 本项目计划研究反推数学中最为活跃的课题- - Ramsey理论的反推数学，特别是各种与n-元关系（n > 2）相关的组合原理，并将考察Ramsey定理的一个较强形式- - Hindman定理的证明论强度。最近几年来，非标准模型方法在反推数学上有一系列异常成功的应用，我们将考察我们的课题与非标准模型的联系，尝试刻画一些二阶命题的一阶理论。在技术上，我们将从一些与反推数学相关可计算性理论问题入手，特别是反推数学与可计算性理论的一个新兴分支- - 算法随机性- - 的关系，并寻求回答反推数学问题的较为统一的技术方案。

反推数学是近年来炙手可热的一个数理逻辑研究领域。在最近的二十年里，可计算性理论的技术极大地推动了反推数学的发展，而反推数学也给可计算性理论的发展注入一股动力。本项目主要围绕组合数学的反推数学展开，同时研究相关的可计算性理论、图论问题和复杂性理论及算法问题。研究工作基本按计划展开，不过过程并非完全顺利，进度略慢，但我们也取得若干深刻且出人意外的成果，并建立起反推数学和数理逻辑的其它研究领域 —— 一阶算术模型论、算法随机性 —— 的联系。在反推数学方面，我们引入一种分析组合原理强弱的新角度，建立这种新视角与证明论强度的联系，并运用它统一地重新证明了若干已知结论，同时也得到若干新结论；我们从组合原理的一阶理论切入，研究反推数学与一阶算术模型论的联系，并进一步发展了一些经典的算术模型论方法；在图论问题上，我们对适合反推数学研究的图论问题做了一些探索，主要针对有向图和特殊的有向图——竞赛图展开；同时我们考察了图论中的复杂性和算法问题。