2012 Fiscal Year Annual Research Report
| Project/Area Number |
12J00654
|
|---|
| Research Institution | Kobe University |
|---|
Principal Investigator |
倉橋 太志 神戸大学, 大学院・システム情報学研究科, 特別研究員(DC2)
|
|---|
| Keywords | 数理論理学 / 不完全性定理 / 形式的算術 / 可証性述語 / 証明可能性論理 / Yabloの逆理 |
|---|
| Research Abstract |
本研究の目的は,形式的算術の中において形式的体系の証明可能性を表現する論理式である可証性述語の性質について調べ,それを通じて不完全性定理および形式的な演繹体系の理解を深めることである.
1.述語証明可能性論理について
述語証明可能性論理の研究を通じて可証性述語の性質を理解する試みを行った.述語証明可能性論理が可証性述語の取り方に依存するというArtemovによる結果が,ペアノ算術の部分理論IΣ_iにも適用できることを示した.更に自然数i,j(ただし0<i<j)に対して,IΣ_iのある可証性述語が存在して,IΣ_jのどんな可証性述語についてもそれらの述語証明可能性論理には一切の包含関係が成立しないことを示した.
2.不完全性定理について
Yabloの逆理をロッサーの可証性述語を用いて形式化することで得られる命題の独立性について研究を行った.この形式化はΣ_1-「健全な理論に対して独立命題を与えるが,一方Σ_1-健全でない無矛盾な理論に対する独立性は証明述語の取り方に依存することをGuaspari-Solovayによる手法を用いて示した.この状況はうそつきの逆理に基づく不完全性定理の証明のものと異なるため,本成果は独立命題の構造および逆理の分析に新たな視点を与えると考えられる.
3.S. Artemov教授(NY市立大),E. Nogina教授(NY市立大)を招聘して研究集会を開き,本研究に関係する議論を行った.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
述語証明可能性論理および不完全性定理についてそれぞれ新たな結果が得られ,合計2本の論文を投稿することができたため.一方,算術的完全性定理の拡張に関する研究は具体的なアイディアは得られたが成果を出すには至らなかったので計画以上とはいいがたい.
|
| Strategy for Future Research Activity |
本年度招聘したArtemov教授から,述語証明可能性論理に関して,証明可能性の様相演算子をもつ形式的算術を研究すると良いとのアドバイスをいただいた.彼の提唱した証明の論理の枠組みを織り交ぜながら,アドバイスを参考に新たなアプローチを模索していきたい.
|
