2020 Fiscal Year Annual Research Report
Uniform computability and constructive derivability between existence sentences
| Project/Area Number |
18K13450
|
|---|
| Research Institution | Meiji University |
|---|
Principal Investigator |
藤原 誠 明治大学, 研究・知財戦略機構(生田), 研究推進員(客員研究員) (20779095)
|
|---|
| Project Period (FY) |
2018-04-01 – 2021-03-31
|
| Keywords | 計算可能数学 / 構成的逆数学 / 逆数学 / 直観主義算術 / 存在定理 |
|---|
| Outline of Annual Research Achievements |
研究期間全体を通し，主に以下の2つの研究成果を得た:
1. 計算可能数学における存在定理の間の相対的一様計算可能性を，直観主義論理に基づいた有限型算術における相対的証明可能性を用いて部分的に特徴付けるメタ定理を得た．さらに，弱ケーニヒの補題とその変種，無限グラフ理論における結婚定理，実解析学における中間値の定理らの関係性についての計算可能数学や構成的逆数学における結果やその証明を詳しく分析し，上記のメタ定理がそれらの大部分に対して適用可能であること，及び一部については適用可能ではないことを示した．これにより，多くの類似結果が知られていた計算可能数学と構成的逆数学の両者の関連について，新たなる知見をもたらすことができた．
2. 計算可能数学や逆数学における存在定理の列版の相対的一様計算可能性と構成的証明可能性の関係について解析し，列版の相対的一様計算可能性は可算選択公理を認める構成的証明可能性に対応することを裏付ける新たなるメタ定理を得た．また，計算可能数学及び構成的逆数学の双方の文脈において詳しく調べられている弱ケーニヒの補題と非構成的原理LLPOの同等性証明を上記のメタ定理の枠組みで詳しく解析し，同メタ定理が計算可能数学及び構成的逆数学の両者の文脈における同等性証明の間の非自明な変換を与えるものであることを実証した.
本年度は， 研究成果を当該分野の研究コミュニティーに幅広く周知し，さらなる発展の可能性を模索した．特に，2つの国際研究集会(COVID-19感染拡大の影響によりオンライン開催)において上記の研究成果について発表した他，研究滞在中のLMUミュンヘンにおいて関連分野の研究者と積極的に議論を交わした．その中で， 計算可能数学における存在定理の間の一様計算可能性は，構成的逆数学よりもむしろプログラム抽出と関連が深いのではないか，という新たなる予想が生まれた．
|
