| 研究概要 |
本研究の目的は,形式的算術の中において形式的体系の証明可能性を表現する論理式である可証性述語の性質について調べ,それを通じて不完全性定理および形式的な演繹体系の理解を深めることである.
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市立大)を招聘して研究集会を開き,本研究に関係する議論を行った.
|
