2016 Fiscal Year Research-status Report
多重視点の証明解析による逆数学の汎用化・深化とその応用
| Project/Area Number |
16K17640
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
横山 啓太 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (10534430)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 逆数学 / ラムゼイの定理 / 証明論 / 原始再帰的関数 |
|---|
| Outline of Annual Research Achievements |
平成28年度は諸種の組み合わせ論の強さを逆数学の手法の構築に力を注いだ。結果として本研究課題の最大の目標としていた、ラムゼイの定理に関する逆数学的分析について、特に証明論的強さの視点からの分析を完了することができた。Patey博士(UC Berkeley)との共同研究により、2組2色のラムゼイの定理の証明論的な強さの核となる部分を抜き出した、groupingと呼ばれる新たな組み合わせ命題についてマサイアス強制法を用いた解の構成法と再帰的飽和モデルを用いてその証明論的強さを確定し、これを応用してラムゼイの定理そのものの証明論的強さが原始再帰的関数で特徴付けられることを証明した。結果についた論文は学術論文誌に投稿中である。またこの結果とヒルベルトの還元主義プログラムについての関連性はウェブジャーナル Quanta Magazine の記事 Mathematicians Bridge Finite-Infinite Divide でも紹介されている。
さらに、これと並行して2組多色のラムゼイの定理の証明論的強さの分析も進め、Slaman教授(UC Berkeley)との共同研究により2組多色のラムゼイの定理の証明論的強さが多重再帰的関数で特徴付けられることを証明した。結果をまとめた論文を現在執筆中である。
これらの他に、算術における論理公理の分離問題をクリプキモデルと超準モデルの手法を組み合わせて一般的に解く手法の構築、算術における証明のサイズを組み合わせ論の手法により分析する研究、完備距離空間における不動点定理の逆数学的強さの分析等の研究を並行して進めており、いずれについてもいくつかの見通しの良い結果を得て29年度も継続して研究を行う予定である。
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本研究課題全体を通じての最大の課題であったラムゼイの定理の証明論的強さを確定する未解決問題が解決した。さらにそこで用いた手法を拡張することでより精密な証明論的強さの分析や他の組み合わせ命題への応用など多くの可能性が見いだされ、既にいくつかについては成果が上がっている。また付随して海外の多くの研究者との共同研究の枠組みを拡大することができた。
|
| Strategy for Future Research Activity |
今後の研究では28年度に得られた手法を精密化、一般化しより多くの応用を得ることが重要と考える。用いた手法は証明論・逆数学分野における新たなツールとして研究者の間で認識が広がっているものの、実際に有効活用する際には精密な有限組み合わせ論の議論が必要となり、技術的な汎用性はまだ発展途上である。今後は既存の定理に新手法を用いた再証明を与える等、汎用性を引き上げる努力が必要であると思われる。また並行して進めている論理公理の強さのモデル論的手法による分析も着実に進展している。これらをふまえ、研究計画でもあげているように計算機科学の視点も取り入れながら手法の融合と新たな視点の構築を目指したい。
|
| Causes of Carryover |
3月に予定していた米国出張(3週間)を先方の都合により4月に延期した。また、パソコンを購入予定であったが当面所持している物で補えたため、また旅費逼迫のため購入を控えた。
|
| Expenditure Plan for Carryover Budget |
4月の米国出張に次年度配分額と合わせて使用予定である。出張予定を1ヶ月ずらした以外で計画に大きな変更はない。
|
