2023 Fiscal Year Final Research Report
Approaching proof theory from the viewpoint of proof size
Project/Area Number |
19K03601
|
Research Category |
Grant-in-Aid for Scientific Research (C)
|
Allocation Type | Multi-year Fund |
Section | 一般 |
Review Section |
Basic Section 12030:Basic mathematics-related
|
Research Institution | Tohoku University (2021-2023) Japan Advanced Institute of Science and Technology (2019-2020) |
Principal Investigator |
|
Project Period (FY) |
2019-04-01 – 2024-03-31
|
Keywords | 証明論 / 逆数学 / 計算可能性理論 / ラムゼイの定理 / 算術のモデル理論 / 強制法 / 反映原理 |
Outline of Final Research Achievements |
We developed a new field of proof theory and its theoretical framework, and explored its applications to mathematical logic and theoretical computer science. Specifically, we obtained the following results: 1. We established a method for analyzing the quantitative information of proofs and showed that the length and size of proofs can be a measure to subdivide the proof-theoretic strength. 2. We discovered that Ekeland's variational principle requires a strong axiom system, which provided a new approach to proving the difficulty of problems in analysis. 3. We showed that the linear time hierarchy is strictly smaller than nondeterministic exponential linear time under the assumption of the provability of the MRDP theorem in weak arithmetic.
|
Free Research Field |
数理論理学
|
Academic Significance and Societal Importance of the Research Achievements |
本研究で得られた、証明の複雑さに関する様々な尺度からの知見は、証明論と計算可能性理論の分野間の結びつけを強化し発展に貢献するものである。また、本研究で扱われたラムゼーの定理の証明論視点からの量的情報分析は、組み合わせ論への応用も期待される。 さらに、本研究で得られた成果は、数学の基礎に関する理解を深めることにもつながる。数学の基礎に関する研究は、数学全体の発展を支えるものでもある一方、数学と計算機科学を直結させる具体的な手法を提供する物でもある。自然科学の発展に寄与するだけでなく、計算機による検証や人工知能の安全性の担保等に対する具体的技術の基盤となることも期待される。
|