2023 Fiscal Year Research-status Report
Constructive reverse mathematics and computational content of mathematical theorems
| Project/Area Number |
21KK0045
|
|---|
| Research Institution | Toho University |
|---|
Principal Investigator |
石原 哉 東邦大学, 理学部, 訪問教授 (10211046)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
河井 達治 高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
横山 啓太 東北大学, 理学研究科, 教授 (10534430)
根元 多佳子 東北大学, 情報科学研究科, 准教授 (20546155)
藤原 誠 東京理科大学, 理学部第一部応用数学科, 助教 (20779095)
|
|---|
| Project Period (FY) |
2021-10-07 – 2026-03-31
|
| Keywords | 逆数学 / 証明論 / 構成的集合論 / 構成的算術 / 構成的位相数学 / 論理的公理の階層 / 算術的超限再帰 |
|---|
| Outline of Annual Research Achievements |
本研究課題の算術における逆数学・集合論における逆数学・様々な公理の解析・プログラム理論の構築の研究においてそれぞれ次の実績があった。
【算術における逆数学】英国・リーズ大学の研究者と東北大学の博士課程学生とともに可述・非可述の中間領域に対応する解析学の命題の探索を継続的に行い、ドイツ・ヴュルツブルク大学の研究者とともに順序数解析と逆数学における組み合わせ命題解析の複合的手法について議論を開始した。また、弱ケーニッヒの補題（WKL）と連続性定理の関係に関する研究を行った。
【集合論における逆数学】英国・リーズ大学の研究者とともに構成的集合論における実現可能性解釈に関する研究を行った。イタリア・パドヴァ大学の研究者とともに構成的ポイントフリー位相数学におけるコーシー有限列を用いた実数の位相構造に関する研究、およびドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究者を加えサンビンが提案した基本対の概念を参考に構成的一様空間を定義しその完備化・積を与えるとともにそれらのもつ自然な性質を示した。
【様々な公理の解析】ケーニヒの補題（KL）とWKLの差を埋める公理を構成的逆数学の観点から解析し、同公理を特徴付ける関数の存在公理を特定した。また、KL とその亜種 KL!, KL!! の特徴づけに関する研究を行った。研究代表者・分担者に静岡大学の研究者を加え様々な公理の解析における最大の難所である公理間の導出不可能性を示すための有用なモデル論的手法を提案し整備した。
【プログラム理論の構築】ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究者とともにケーススタディとして擬距離に基づく構成的一様空間論の定理証明・プログラム抽出系（Minlog）への実装を行い、また基本対の概念を参考した構成的一様空間論の実装可能性について議論を開始した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
【算術における逆数学】計算可能性と証明論・逆数学の視点を組み合わせた研究テーマが広がりを見せ、大きなブレークスルーはないまでも着実に結果が積み上がっている。また、いくつかの関連論文の出版が完了し次なる国際共著論文の執筆にも着手しており継続的な成果発表が見込まれる。弱ケーニッヒの補題（WKL）と実関数の連続性定理に関する研究では、WKLの仮定を再帰的内包公理（RCA）に弱めることを目的としていたが従来の証明の分析に留まった。
【集合論における逆数学】構成的集合論における実現可能性解釈の応用例についての論文が出版され、さらに二重否定翻訳の応用した結果も得られた。WKLと実関数の連続性定理に関する研究では「コーシー有限列による表現が符号付きビット表現を用いた実数の位相表現と同等である」という予想を立てたが予想の厳密な証明には至っていない。構成的一様空間論は順調に構築できている。
【様々な公理の解析】構成的逆数学におけるケーニッヒの補題（KL）などの特徴づけの論文も受理され、さらに他の結果についての論文を準備中である。コロナ禍や円安の影響により海外の研究拠点をそれなりの頻度で直接訪問することが難しく未だ国際共同研究の開始には至っていない。
【プログラム理論の構築】構成的一様空間論を用いたケーススタディにとどまっており理論の構築の糸口が得られたのみである。
|
| Strategy for Future Research Activity |
【算術における逆数学】ラムゼイの定理の逆数学に関連する未解決問題への新たなアプローチが提唱され研究が活性化しているが、この研究テーマに順序数解析的手法を導入することで新たなブレークスルーが得られるのではないかと見込んでいる。 弱ケーニッヒの補題（WKL）と実関数の連続性定理に関する研究の目標達成には新たな観点が必要と予想されるため、問題の否定的解決の可能性も含めて従来より視野をひろげて調査・研究を行う。
【集合論における逆数学】構成的集合論における二重否定翻訳および実現可能性解釈を応用して、さらなる体系の無矛盾性・等価性の証明を試みる。予想「コーシー有限列による表現と符号付きビット表現を用いた実数の表現が同等である」に関しては、今までの研究により証明の見通しは立っているためイタリア・パドヴァ大学の研究者の協力を得て証明を試みる。今までに構築した構成的一様空間論を積分論やバナッハ空間の双対空間の解析に応用する。
【様々な公理の解析】ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究グループを直接訪問し本研究課題の研究成果について報告するとともに共同研究の構想を練る。構成的逆数学における帰納法の役割をケーニッヒの補題（KL）や計算可能性理論の観点から明らかにする。
【プログラム理論の構築】プログラム理論に関する国際研究会議に参加し関連研究についての情報収集を行い、新たな共同研究の具体的な構想を練る。ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究グループを直接訪問し、今までのケーススタディを参考にプログラム理論に関する共同研究を立上げる。
|
| Causes of Carryover |
海外出張旅費の先方負担、分担者の健康上の理由による海外出張の中止、分担者の異動にともなう教育・運営負担の増加、双方の調整不良などのため、次年度使用額が生じている。次年度は英国・リーズ大学、ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘン、イタリア・パドヴァ大学を中心に研究代表者・分担者ともに数週間の直接訪問による共同研究を予定しており、海外研究者の招へいも調整中である。航空券が高騰して海外出張旅費が多くかかる見込みのため引き続き効率の良い使用を心がける。
|
