2020 Fiscal Year Research-status Report
Computability theory on intuitionistic logic and its application to constructive reverse mathematics
| Project/Area Number |
18K03392
|
|---|
| Research Institution | Hiroshima Institute of Technology |
|---|
Principal Investigator |
根元 多佳子 広島工業大学, 環境学部, 准教授 (20546155)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | 直観主義論理 / 算術 / 逆数学 |
|---|
| Outline of Annual Research Achievements |
2020年度の研究では、直観主義論理上の算術の体系における非構成的原理間の関係についての研究および構成的逆数学のための形式体系の間の関係について研究を行った。
直観主義論理上の算術の体系における非構成原理間の関係については、直観主義論理のモデルとして広く使われるKripkeモデルの手法を算術の体系まで拡張し、Σ^0_1命題についての二重否定除去則、ド・モルガンの法則、排中律などの強さが真に異なることを示した。この研究は石原・藤原・鈴木・横山との共同研究で現在論文を投稿中である。
構成的逆数学のための形式体系の間の関係についての研究では、これまでに様々な研究者が提案してきた構成的逆数学のための算術の体系について、それらの間の翻訳可能性を明らかにした。これらの体系の差異は主に帰納法原理をどこまで認めるかと、言語にどれだけの関数を含むか、選択公理をどこまで認めるかで、証明論的な強さによって分類される。本研究の結果、これまでに提案されてきた7つの体系が証明論的な強さで3種類に区分されること、特に帰納法などに制限のある体系においての翻訳の手法が明確になった。後者については、これまで一般的な手法は帰納法などの公理図式に対して制限のない体系か、または古典論理上の体系でないとうまく使えないものであった。今回の研究で用いた手法では、翻訳において論理式の複雑さをなるべく保つことができるため、公理図式が制限された直観主義論理上の体系でも有効である。
|
| Current Status of Research Progress |
Current Status of Research Progress
3: Progress in research has been slightly delayed.
Reason
直観主義論理上の逆数学の研究や非構成原理の研究という観点からは研究実績に記載の通り進展があったといえるが、直観主義論理上の計算可能性理論の研究については進捗があまりない現状である。これは、研究代表者の異動およびコロナ禍による授業形態のオンライン化による授業負担の急な増加、研究会や他研究機関へ訪問して他の研究者と議論や情報交換をする機会が極端に減ったことによるものである。
|
| Strategy for Future Research Activity |
2021年度は直観主義論理上の計算可能性理論の研究を進めることに注力する。特に優先法およびΣ^0_1までの次数の直観主義論理上での振る舞いを明らかにすることを目指す。
|
| Causes of Carryover |
研究計画当初から国内外の研究会や研究機関への旅費に多くを割く予定であったが、2019年度末からのコロナ禍でほとんどが中止となったため次年度使用額が多額に発生した。
|
