2022 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 – 2024-03-31
|
| Keywords | 数理論理学 / 数学基礎論 / 不完全性定理 / 証明可能性述語 / 様相論理 / 形式的算術 / 証明可能性論理 |
|---|
| Outline of Annual Research Achievements |
(1) 通常，第二不完全性定理の証明においては証明可能性述語は導出可能性条件 D1, D2, D3 を満たすことが想定されているが，他方で Rosser 証明可能性述語など D2 や D3 を満たさないものもあり，そのような証明可能性述語を用いて導出可能性条件と第二不完全性定理の成立に関する詳細な分析をこれまでに行ってきた．今回は証明可能性述語に最低限要求したい D1 以外の一切の条件を満たさない証明可能性述語について，様相論理の観点から分析を行った．具体的には，そのような証明可能性述語に対応する様相論理が，Fitting らによる非正規様相論理 N とちょうど一致することを証明した．更に，N の拡張である N4, NR, NR4 について同様の分析を行った．
(2) 上述の (1) の研究に続いて，Hilbert と Bernays による導出可能性条件 M（φ→ψ が証明できれば Pr(φ)→Pr(ψ) も証明できる）を満たす証明可能性述語について，様相論理の観点から分析を行った．非正規様相論理 MN がちょうどそのような証明可能性述語の様相論理であることをはじめとして，MN4, MNP, MNP4, MND についても同様の分析を行った．本研究は金沢大学の小暮晏佳氏との共同研究である．
(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
今年度は特に昨年度に計画していた通り，「証明可能性述語に対応する非正規様相論理に関する研究」という，新たな研究領域を創出し，そしていくつかの基本的な成果を得ることができた．本研究を通して，今まで曖昧にしか語ることのできなかった現象に明確な説明を与えることができるなど，不完全性定理および証明可能性への理解について進展があった．また，本研究に取り組むことによって，不完全性定理の観点から非常に重要な課題をいくつも発見することができた．こうした今後の研究の礎を築くことができたという点でも，有意義であったといえる．得られた研究成果については学術雑誌に投稿した．
|
| Strategy for Future Research Activity |
今年度の研究によっていろいろと重要な課題を見つけることができたため，まずはそういった課題について分析を進める．また，弱い算術における第一不完全性定理を通じて証明可能性の性質をとらえる研究について進展があったため，今後はこの方面でも研究を推し進めていきたい．
|
| Causes of Carryover |
コロナウイルス感染拡大により学会や研究集会への出張旅費としての使用が難しかったため。
書籍の購入や研究打ち合わせなどに効率よく使用する予定である。
|
