2020 Fiscal Year Research-status Report
Approaching proof theory from the viewpoint of proof size
| Project/Area Number |
19K03601
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
横山 啓太 北陸先端科学技術大学院大学, 先端科学技術研究科, 講師 (10534430)
|
|---|
| Project Period (FY) |
2019-04-01 – 2022-03-31
|
| Keywords | 数理論理学 / 証明論 / 算術の超準モデル / 逆数学 / 数学基礎論 / 組み合わせ論 / 強制法 / クリプキモデル |
|---|
| Outline of Annual Research Achievements |
令和2年度の主な研究成果は「1.算術の超準モデルにおける新しい同型定理の発見とその応用」「2.弱い算術体系における組み合わせ命題分析の新手法の構築」「3.算術体系の分析へのクリプキ意味論の適用」があげられる．前年度より，本研究課題に直接関係するいくつかのテーマについて，シンガポール国立大学のT.L.Wong博士およびワルシャワ大学のL. Kolodziejczyk博士らの研究グループと継続した研究プロジェクトを進めており，1,2はその成果となっている．
1は交付申請書のI,IIに関連する幅広い帰結を持つモデル理論的定理の発見である．弱ケーニッヒ補題をもつ算術体系WKL0*の可算モデルが原始再帰法の公理を満たさないとき，その2階部分の構造は同型を除いて一意に定まると言う主張である．この定理は帰納法公理の制限された状況下において2階算術の解析階層が部分的に崩壊し，自然数の部分集合に関する2階の命題が計算可能性の表現を用いた1階の命題に書き換えられてしまうことを示している．その帰結として，算術の証明論におけるTowsnerの問題等が解決され，また算術体系間の保存性証明と計算可能次数の理論の算術における形式化の間の非常に密接な関係が明らかとなった．
2では前年度に構築した交付申請書IIの研究課題に，本研究課題の主眼である証明の長さに着目したフレームワークを一部適用するなどにより，ラムゼイの定理の振る舞いをこれまで既知の結果よりもさらに弱い公理系の下で分析した．ラムゼイの定理に関する逆数学の未解決問題に対する多くの情報をもたらすと共に，帰納法公理・採集原理と特異基数で表現される超準モデルの関係性について調べた1990年代のKayeによる一連の研究を組み合わせ命題と関連付けた．
3では直観主義算術体系の分離や算術体系間の保存性証明における証明の長さの分析にクリプキ意味論の手法を導入した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
本年度の研究で発見されたWKL0*の超準モデルにおける同型定理は1階算術体系と2階算術体系の関係性，計算可能性次数の理論と逆数学の関係性について非常に多くの情報をもたらす根源的な原理であることが分かった．その応用の幅は広く，既知の算術体系間の保存性定理や分離定理に見通しの良い証明を与える一方，2階算術の証明論におけるTowsnerの問題，WKL0*の証明の長さに関する問題，組み合わせ命題ラムゼイの定理の算術体系下における計算可能性など多くの問題を解決・進展させた．また定理自身のさらなる一般化も見込めており，今後さらに多くの帰結を得ることが期待できる．
また，オンラインによる新たな研究交流環境の構築と共同研究体制の確立により，ワルシャワ大学の研究グループとの間で非常に密接な共同研究体制を取ることが可能となり，他にも多くのオンラインセミナーを通じた研究交流をはかることが出来た．オンラインでの共同研究・研究交流には限界もあるものの，パンデミックの状況下において今までよりも一面において強力な国際共同研究基盤を得られたことは今後の研究網の拡充にも大きく役立つ物となる．
|
| Strategy for Future Research Activity |
まずは今年度得られた多くの成果について既に執筆中の論文を随時完成させ発表を進めていく．得られた成果が多様な方向に適用できることが分かったため，それらを整理して洗練することで今後の研究課題の発掘にもつなげていく．
またパンデミックの収束を待って対面での共同研究を再開することを通じて，共同研究の中断を余儀なくされている交付申請書のIII, VIに関連する共同研究を再加速させていく．
|
| Causes of Carryover |
パンデミックの影響により，予定していた国内外の会議への直接参加・海外からの研究者の招聘をほとんど行うことができず，その多くをオンライン等で代替して行った．本年度予定していたそれらの対面での共同研究・研究打ち合わせは翌年度にパンデミックの収束を待って集中して行う計画である．
|
