形式的算術の証明可能性について

点击翻译按钮获取中文摘要

本研究の目的は、形式的体系の証明可能性を表現する論理式である可証性述語の形式的算術における振る舞いについて調べ, そのことを通じて不完全性定理や形式的算術の超準モデルなどの理解を深めることである.1. ロッサーの可証性述語についてロッサー可証性述語に基づくヘンキン文および反映原理に関する研究を行った, まず, 独立なヘンキン文をもつかどうかが可証性述語の取り方に依存することを示し, Halbach and Visser (2013)による問題を解決した. また, Shavrukov (1991)による問題を解決することで, 反映原理が通常のものと同値でないようなロッサー可証性述語の存在を示し, Goryachev (1989)による結果と合わせて, それらの同値性がロッサー可証性述語の取り方に依存することを明らかにした. これらの結果により, ロッサー可証性述語の性質の理解だけでなく, 形式的証明そのものの構造の理解が深まることが期待される.2. 算術の超準モデルにおける証明可能性ついて本研究はこれまでほとんど行われていなかった, 算術の超準モデルにおける証明可能性について分析するものである. 本年度は(a)Con2のモデルでも証明可能的極大でもないようなペアノ算術の超準モデルの存在, (b)ペアノ算術の超準モデルである任意の始切片において証明可能なものが実際より増えているような超準モデルの存在, (c)ペアノ算術の各無矛盾な完全拡大を何らかの超準モデルにおいて定義するようなロッサー可証性述語の存在, を示した. 本結果により, 超準モデルにおける証明可能性や証明の構造に関する基本的な性質が明らかとなった.