研究課題/領域番号 |
19K03601
|
研究種目 |
基盤研究(C)
|
配分区分 | 基金 |
応募区分 | 一般 |
審査区分 |
小区分12030:数学基礎関連
|
研究機関 | 東北大学 (2021-2023) 北陸先端科学技術大学院大学 (2019-2020) |
研究代表者 |
横山 啓太 東北大学, 理学研究科, 教授 (10534430)
|
研究期間 (年度) |
2019-04-01 – 2024-03-31
|
研究課題ステータス |
完了 (2023年度)
|
配分額 *注記 |
4,290千円 (直接経費: 3,300千円、間接経費: 990千円)
2021年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2020年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
2019年度: 1,560千円 (直接経費: 1,200千円、間接経費: 360千円)
|
キーワード | 証明論 / 逆数学 / 計算可能性理論 / ラムゼイの定理 / 算術のモデル理論 / 強制法 / 反映原理 / 超準モデル / パラメータ付き計算量 / 数理論理学 / 算術の超準モデル / 数学基礎論 / クリプキモデル / 組み合わせ論 / 算術 |
研究開始時の研究の概要 |
証明の最も代表的な量的情報である長さ・サイズは、数学における証明の難しさや複雑さを測定する最も直感的な尺度と考えられる。しかし証明のサイズは公理系の取り方に強く依存し、証明の複雑さを公理の強さ以上には反映しないと考えられてきた。実際、公理の証明論的な強さが異なると証明のサイズを自由に変化させられるような命題の例が存在する、というEhrenfeucht/Mycielskiの定理が知られている。しかし、この定理の詳細な分析から証明のサイズが証明論的強さを細分化するような尺度になりうることがわかってきた。本研究では、この「細分化尺度としての証明の量的情報」の理論構築・普遍量化を目指しその応用を探る。
|
研究成果の概要 |
証明論における分野融合的な手法を用いて、証明論の新分野開拓・理論構築を行い、数理論理学や理論計算機科学への応用を探った。具体的には、以下の成果が得られた。 1. 証明の量的な情報の分析手法を確立し、証明の長さやサイズが証明論的強さを細分化する尺度となりうることを示した。2. 変分問題における Ekeland の定理が強い公理系を要請することを発見し、解析学における未解決問題の難しさの証明に新たなアプローチを提供した。3. 弱い算術における MRDP 定理の証明可能性を仮定した下で、線形時間計算可能階層が非決定指数線形時間問題よりも真に小さいことを示した。
|
研究成果の学術的意義や社会的意義 |
本研究で得られた、証明の複雑さに関する様々な尺度からの知見は、証明論と計算可能性理論の分野間の結びつけを強化し発展に貢献するものである。また、本研究で扱われたラムゼーの定理の証明論視点からの量的情報分析は、組み合わせ論への応用も期待される。 さらに、本研究で得られた成果は、数学の基礎に関する理解を深めることにもつながる。数学の基礎に関する研究は、数学全体の発展を支えるものでもある一方、数学と計算機科学を直結させる具体的な手法を提供する物でもある。自然科学の発展に寄与するだけでなく、計算機による検証や人工知能の安全性の担保等に対する具体的技術の基盤となることも期待される。
|