2020 Fiscal Year Research-status Report
Research of formal provability by means of the investigation of incompleteness theorems
| Project/Area Number |
19K14586
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
倉橋 太志 神戸大学, システム情報学研究科, 准教授 (10738446)
|
|---|
| Project Period (FY) |
2019-04-01 – 2023-03-31
|
| Keywords | 数学基礎論 / 数理論理学 / 不完全性定理 / 証明可能性 / 形式的算術 / 様相論理 / 証明可能性述語 / 部分的な保存性 |
|---|
| Outline of Annual Research Achievements |
(1)昨年度の研究において導入した，解釈可能性論理ILや保存性論理CLの部分論理に対する不動点の性質(FPP)，不動点の一意性(UFP)，クレイグの補間性(CIP)の成立状況について網羅的な分析を行い，特に重要な12個の論理に関してはそれぞれの性質の成立・不成立の状況を完全に調べることができた．本研究により，特にILの各公理がどのような役割を担っているのかの理解が深まった．神戸大学の岩田荘平氏，千葉大学の大川裕也氏との共同研究である．
(2)ILやCL，およびその拡大論理は関係意味論に関して強完全ではない．本研究では2重位相空間を用いたILやCLに対する位相的意味論を導入し，Shehtman による超ブーケの概念を拡張することによって，これらの論理に対する位相的強完全性を証明した．神戸大学の岩田荘平氏との共同研究である．
(3)ペアノ算術の排中律を算術的階層に沿って弱めることで得られる諸理論の構造の分析を行うことで，古典算術及び直観主義算術の証明可能性の構造の理解を深める研究を進めた．特に冠頭標準形の詳細な分析を行い，Akama, Berardi, Hayashi and Kohlenbach (2004) の結果のギャップを埋め，更に得られた結果が最適であることを証明した．これは明治大学の藤原誠氏との共同研究である．
(4)証明可能性の様相述語論理はいろいろな結果がきれいには成立しないことが知られている．特にペアノ算術の述語証明可能性論理がΠ_2-完全であるという Vardanyan の定理が決定的である．本研究では Vardanyan の定理の証明において本質的である Artemov の補題を用いて述語証明可能性論理間の包含関係が成立するための必要条件をいくつか示した．また，同様の手法により，Σ_1述語証明可能性論理間の包含関係が成立するための必要十分条件も与えた．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
部分保存性に関する研究の，特に様相論理からのアプローチについていろいろと研究を進めることができた．同様に，証明可能性述語そのものに関しても様相述語論理における新たな結果を得ることができた．算術そのものに関しても，直観主義算術と古典算術の証明可能性に関する諸結果を得ることができた．
|
| Strategy for Future Research Activity |
今後も引き続き様相論理からのアプローチでの研究も進めていく．また，直観主義算術と古典算術に関する研究も証明可能性の構造の理解という観点から非常に得るものが多いため，引き続き今後も明治大学の藤原誠氏との共同研究を進めていく．昨年度は算術における証明可能性述語の役割に関する研究の勢いを弱めてしまったので，その方面もぜひ進めていきたい．
|
| Causes of Carryover |
異動による研究環境変化およびコロナウイルス感染拡大による．
次年度も学会や研究集会への出張旅費としての使用を期待するが，感染拡大状況によると思われる．
|
