限定算術体系におけるさまざまな命題の証明可能性について,以下の2つのアプローチで考察を行った. 1. 竹内と安本が考案した強制法による算術モデルの構成を元に,鳩の巣原理などの算術体系からの独立性のための条件を与えた. 2.行列式,行列の階数,パフィアンなどの線形代数学で扱われる関数の高速アルゴリズムに基づいて,弱い湾術体系においてそれらの性質の証明可能性を考察した. 特に.2においては階数の様々な定義の同値性証明がNC^2回路程度の算術体系で可能であることを示し,またパフィアンのいくつかの性質の同値性などがさらに弱い体系で証明可能であることを示した.
|