2021 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)φ∨ψが証明可能ならばφかψが証明できる、という選言特性とそのバリエーションは直観主義論理、様相論理、または不完全性定理というそれぞれ異なる文脈において議論されてきた。形式的算術に様相記号を加えて得られる様相算術において、既存の結果を統合・強化する研究を行った。結果として Friedman and Sheard(1989)の定理の拡張や、様相選言特性の意味論的特徴づけなどが得られた。本研究は奥田幹との共同研究である。
(2)Σ_1関係の弱表現可能性を形式的算術において形式化することで得られるFGH定理は、任意のΣ_1文がConのもとでPr(φ)という形の文と同値であることを主張する。理論Tにおいて証明も反証もできないような文としてどのような形のものが取れるのか、という問いに対するアプローチとして、本研究では特に上述のφがどのような形の文としてとれるのか、について古典命題論理および様相論理の観点から分析を行った。
(3)PAがHAにΣ_k論理式に対する排中律Σ_k-LEMを加えた理論においてΠ_{k+2}-保存的であることが知られている。今回はPAがHAにΣ_k-LEM以外の論理公理を加えた理論においてどの程度の保存性が成立するのか、またどの程度の保存性が成立すればどのような論理公理や規則が成立するのかを体系的に分析した。本研究は明治大学の藤原誠氏との共同研究である。
(4)解釈可能性論理ILに公理Pを加えた論理の算術的完全性が知られている。本研究はILの部分論理IL^-にPを加えた論理IL^-(P)の諸性質を分析することで、Pがよい振る舞いをすることを明らかにするものである。結果として、IL^-(P)がカット除去可能なシークエント計算をもつこと、関係意味論のベースとなること、算術的完全であることが示せた。岩田荘平氏（神戸大学）および大川裕矢氏（千葉大学）との共同研究である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
形式的算術の証明可能性に関して、不完全性定理を通じることを基本として、semi-classical な算術、様相算術、様相論理、などさまざまなアプローチによって形式的算術の証明可能性を理解する研究を進めることができた。特に様相算術はこれまでの既存研究は□を informal provability で解釈する文脈のみで行われていたが、今回の研究によって□を証明可能性述語で解釈する場合にも様相算術の枠組みが意味を持つことが分かったという点で、進展が大きかったように感じる。
研究活動自体はオンラインではあるが、国内外の研究者と研究討論を行う機会にも恵まれた。また、得られた研究成果については学術雑誌に投稿した。
|
| Strategy for Future Research Activity |
第二不完全性定理と密接に関わっている導出可能性原理について更に詳しく分析を行うことを主眼に、正規様相論理ではない様相論理に対する算術的完全性を証明する手法の確立なども目指す。
コロナ禍ではあるが、引き続き国内外の研究者と討論をしつつ研究を進めていく予定である。
|
| Causes of Carryover |
コロナウイルス感染拡大による。
次年度も学会や研究集会への出張旅費としての使用を期待するが，感染拡大状況によると思われる。
|
