Research of formal provability by means of the investigation of incompleteness theorems
| Project/Area Number |
19K14586
|
|---|
| Research Category |
Grant-in-Aid for Early-Career Scientists
|
| Allocation Type | Multi-year Fund |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Kobe University (2020-2023)
Kisarazu National College of Technology (2019) |
|---|
Principal Investigator |
倉橋 太志 神戸大学, システム情報学研究科, 准教授 (10738446)
|
|---|
| Project Period (FY) |
2019-04-01 – 2024-03-31
|
| Project Status |
Completed (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000)
Fiscal Year 2022: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2021: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2020: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2019: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 不完全性定理 / 数学基礎論 / 数理論理学 / 証明可能性 / 証明可能性述語 / 形式的算術 / 様相論理 / 証明可能性論理 / 部分的な保存性 / クリプキ意味論 / 決定不可能命題 |
|---|
| Outline of Research at the Start |
本研究は，第一不完全性定理，第二不完全性定理にそれぞれ対応する，(1) 形式的体系における決定不可能な文，(2) 形式的体系の証明可能性を表す論理式（証明可能性述語），という二つの対象の構造や性質の分析を主軸におき，形式的証明および形式的証明可能性の構造及び性質を解明することを試みるものである．
(1)様々な決定不可能な命題の振る舞いを分析することによって，理論の証明可能性の構造のもつ性質を明らかにすることを目指す．
(2) 理論の証明可能性が持つ性質のうち本質的なものは何か，そして証明可能性述語が本質的に満たすべき性質とは何かを分析することで，「数学的証明とは何か」という問いの技術的理解を行う．
|
| 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補完性と一様補完性を証明した．本研究は小暮晏佳氏(金沢大)との共同研究である．
|
Report
(5 results)
Research Products
(55 results)
