| 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
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2021: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2020: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2019: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 証明論 / 逆数学 / 計算可能性理論 / ラムゼイの定理 / 算術のモデル理論 / 強制法 / 反映原理 / 超準モデル / パラメータ付き計算量 / 数理論理学 / 算術の超準モデル / 数学基礎論 / クリプキモデル / 組み合わせ論 / 算術 |
|---|
| Outline of Research at the Start |
証明の最も代表的な量的情報である長さ・サイズは、数学における証明の難しさや複雑さを測定する最も直感的な尺度と考えられる。しかし証明のサイズは公理系の取り方に強く依存し、証明の複雑さを公理の強さ以上には反映しないと考えられてきた。実際、公理の証明論的な強さが異なると証明のサイズを自由に変化させられるような命題の例が存在する、というEhrenfeucht/Mycielskiの定理が知られている。しかし、この定理の詳細な分析から証明のサイズが証明論的強さを細分化するような尺度になりうることがわかってきた。本研究では、この「細分化尺度としての証明の量的情報」の理論構築・普遍量化を目指しその応用を探る。
|
| 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.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究で得られた、証明の複雑さに関する様々な尺度からの知見は、証明論と計算可能性理論の分野間の結びつけを強化し発展に貢献するものである。また、本研究で扱われたラムゼーの定理の証明論視点からの量的情報分析は、組み合わせ論への応用も期待される。
さらに、本研究で得られた成果は、数学の基礎に関する理解を深めることにもつながる。数学の基礎に関する研究は、数学全体の発展を支えるものでもある一方、数学と計算機科学を直結させる具体的な手法を提供する物でもある。自然科学の発展に寄与するだけでなく、計算機による検証や人工知能の安全性の担保等に対する具体的技術の基盤となることも期待される。
|
