2021 Fiscal Year Research-status Report
Approaching proof theory from the viewpoint of proof size
| Project/Area Number |
19K03601
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
横山 啓太 東北大学, 理学研究科, 教授 (10534430)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 数理論理学 / 証明論 / 算術の超準モデル / 逆数学 / 数学基礎論 / ラムゼイの定理 / クリプキモデル / 強制法 |
|---|
| Outline of Annual Research Achievements |
令和3年度の主な研究成果は「1.算術の超準モデルにおける同型定理の新活用」「2.弱い算術体系においてラムゼイの定理が導く算術命題構造の解明」「3.算術的超限再帰に関連する公理類と計算可能次数の間の新たな関連性の発見」があげられる．一昨年度より，本研究課題に直接関係するいくつかのテーマについて，シンガポール国立大学の T.L.Wong博士およびワルシャワ大学のL. Kolodziejczyk博士らの研究グループと継続した研究プロジェクトを進めてきたが，1,2は前年度のこれら共同研究による成果の拡張となっている．
1の同型定理は，前年度に得られた超準モデルの強力な新定理(交付申請書のI,IIに関連)である．今年度の研究ではこの定理を詳細に分析して多くの新たな手法・帰結を得た．例として，強制法を利用した弱ケーニッヒ補題に対する新たな多項式時間翻訳の導入とそれによる一意存在命題の保存性に関する田中の予想の解決，2次元ラムゼイの定理の算術的帰結が高々5つの算術的量化記号で表現されるPi_5-論理式で特徴付けられること，弱ケーニッヒの補題やその亜種がIBと呼ばれる公理を満たす算術体系に対する部分的なモデル完全拡大を与えること，等があげられる．
2は前年度に進展させた弱い算術体系におけるラムゼイの定理の分析の完成で，同条件下でのラムゼイの定理の導く帰納法公理・採集原理を多くの場合に確定し，一連の成果を論文に集約した(投稿済み，査読中)．3では研究室の学生との共同により，算術的超限再帰を導くような諸種の公理を計算可能性の視点からの再分析を進めている．いくつかの萌芽的な結果と，算術的超限再帰公理のオメガモデルに関する中心的と考えられる問題の発見に至っている．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
交付申請書にあげた各研究課題に対し，当初の想定よりも幅の広い応用が得られるなど多くの成果を上げることができた．論文による成果発表の他，計算可能性理論の主要会議Computability in Europe 2021での基調講演など成果発表も確実に進めている．
一方で，感染症の収束を待って進める予定であって，関連分野の海外の研究者との成果や手法・問題の共有，新たな共同研究体制の構築，研究連携の強化等はオンラインを通じてある程度の成果は得られたものの，来日予定であったポスドク(外国人特別研究員)の受け入れができなくなったなど，十分とは言えない面があり，研究期間を延長して進めていくこととした．
|
| Strategy for Future Research Activity |
研究の最終年度として，これまでの成果の取りまとめ，成果発表に尽力する．またそれとともに，対面での共同研究の再開の他，研究集会を主催するなど，パンデミック下で停滞してしまった研究連携態勢の立て直しを進め，これまでの研究成果と派生して生じた新たな問題の関連研究者等との共有を図り，関連する最新研究との融合や新しい共同研究課題の創出を目指す．
|
| Causes of Carryover |
共同研究のための海外渡航，ワークショップの対面での開催はパンデミックのため実施を延期した．
|
