| Project/Area Number |
23K03200
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
倉橋 太志 神戸大学, システム情報学研究科, 准教授 (10738446)
|
|---|
| Project Period (FY) |
2023-04-01 – 2028-03-31
|
| Project Status |
Granted (Fiscal Year 2023)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2027: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2026: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2025: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
|
|---|
| Keywords | 不完全性定理 / 数学基礎論 / 数理論理学 / 証明可能性述語 / 形式的算術 / 証明可能性論理 / 様相論理 / 算術のモデル |
|---|
| Outline of Research at the Start |
本研究は，(A) 証明可能性述語と第2不完全性定理，(B) 証明可能性述語の様相論理，という二つの側面からの分析を主軸におき，形式的証明および形式的証明可能性の構造や挙動を解明することを試みるものである．
(A) 第2不完全性定理は無矛盾性を表す文の証明不可能性を主張する定理群であり，これらの背景にある本質的な現象を理解することを目指す．
(B) どの様相論理に対して対応する証明可能性述語をとることができるのか，という問題を通じて証明可能性述語のもつ性質のより精密な理解を目指す．
|
| Outline of Annual Research Achievements |
(1)Rosser型の局所反映原理の保存性：証明可能性述語に基づく反映原理は第二不完全性定理とも関わる重要な研究対象である．Rosser型の局所反映原理の研究はGoryachev(1989)により始められ，Kurahashi(2016)で大きく進んだ．今回は後者の論文において提起された，Rosser型の局所反映原理に対してBeklemishevの保存性定理が成立するか，という問題を中心に，保存性定理の一般化と，保存性定理の成立しないRosser述語の存在証明を行った．本研究は小暮晏佳(金沢大)との共同研究である．
(2)必然化の論理Nの拡張に対する有限フレーム性：Kurahashi(202x)によって全ての証明可能性述語の様相論理がFittingら(1992)の必然化の論理Nと一致することを既に得ている．今回はNに□^mφ→□^nφと適切な推論規則を追加した論理の有限フレーム性の証明を行った．正規様相論理K+□^mφ→□^nφが一般に有限フレーム性を持つかは未解決であり，それに類する問題が解けたことには意義があると思われる．本研究は佐藤雄太（神戸大）との共同研究である．
(3)証明可能性と強制法の様相論理：証明可能性の様相論理GLと強制法の様相論理S4.2はそれぞれ別の文脈において分析されてきた研究対象であるが，証明可能性と強制法は無関係ではない．今回はこれらの研究を統合することを目標に，2重様相論理PFを導入し，それは証明可能性と強制法の様相論理にちょうど一致することを証明した．本研究は高瀬理人（神戸大）との共同研究である．
(4)採集原理のモデル論的特徴づけ：採集原理を満たすモデルの特徴づけは Paris and Kirby(1978)によって与えられているが，今回は特にGaifmanの分割定理に関連する特徴づけを与えた．本研究は南芳明（神戸大）との共同研究である．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
今年度は特に形式的証明可能性の持つ諸性質の分析について，証明可能性述語，様相論理，算術のモデルなどの各方面からの研究を進めることができた．
(1)によって特に反映原理に関する基本的な理解から，細かな技術的な理解までを深めることができたと言える．また(3)はこれまで別々に発展してきた研究領域を統合でき，個人的には非常に意義のある研究成果であると考えている．得られた研究成果についてはいずれも学術雑誌に投稿した．
|
| Strategy for Future Research Activity |
今年度の研究成果(2)については，様々な証明可能性述語の分析に基づく第2不完全性定理の研究に関する様相論理の側面からのアプローチの部分的な進展という位置づけである．今後はこの成果に基づき，形式的証明可能性の様相論理に関する研究を更に進めていく予定である．
|
