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-2022) Kisarazu National College of Technology (2019) |
Principal Investigator |
倉橋 太志 神戸大学, システム情報学研究科, 准教授 (10738446)
|
Project Period (FY) |
2019-04-01 – 2024-03-31
|
Project Status |
Granted (Fiscal Year 2022)
|
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) 通常,第二不完全性定理の証明においては証明可能性述語は導出可能性条件 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 |
今年度の研究によっていろいろと重要な課題を見つけることができたため,まずはそういった課題について分析を進める.また,弱い算術における第一不完全性定理を通じて証明可能性の性質をとらえる研究について進展があったため,今後はこの方面でも研究を推し進めていきたい.
|
Report
(4 results)
Research Products
(39 results)