2023 Fiscal Year Annual Research 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不完全性定理と様相論理に関する進展があった．
(1)弱い算術Rに対するCobhamとVaughtの定理の拡張：Rが本質的遺伝的決定不能であるというCobhamの定理と，それを拡張したRの強実効的分離不能性を示すVaughtの定理(1962)の拡張を行い，また見通しの良い証明を与えた．本研究はAlbert Visser氏(ユトレヒト大)との共同研究である．
(2)Pour-Elの定理とその周辺：CE理論の実効的本質的不完全性と実効的分離不能性を主張するPour-Elの定理(1968)の簡潔な別証明を与え，またそのアナロジーとしてCE理論の実効的本質的遺伝的創造性が強実効的分離不能性と同値であることを証明した．本研究はAlbert Visser氏(ユトレヒト大)との共同研究である．
(3)証明可能性論理Dのシークエント計算：Kushida(2020)による証明可能性論理Sのシークエント計算の体系とそのカット除去に基づき，今回はGLとSの間にある証明可能性論理であるDのシークエント計算の体系とそのカット除去を分析した．本研究は鹿島亮氏(東工大)と岩田荘平氏(愛知学院大)との共同研究である．
(4)2重証明可能性論理GRの補間定理：通常の証明可能性述語とRosser述語に関する2重様相論理GRのCraig補完性はSidon(1994)によって証明されている．今回はGRの部分論理GR^\circとGRに対する新たな関係意味論を導入し，それに基づいてGR^\circとGRのLyndon補完性と一様補完性を証明した．本研究は小暮晏佳氏(金沢大)との共同研究である．
|
Research Products
(16 results)
