本研究において,竹内外史と安本雅洋が提案した,限定算術の超準モデル上での強制法の理論を体系的に整備し,従来は多項式時間計算可能クラスとの関係においてのみ示されていた結果を,そのいくつかの部分クラスでも同様に示した. また,従来の理論においては極めて弱い論理式のクラスの扱いのみが示されており,例えば鳩の巣原理のような命題のモデルにおける取り扱いについては不可能であったが,より強い論理式を扱う方法を与えた. さらに,独立命題の候補について考察し,線形代数学におけるいくつかの命題のよわい算術体系における証明可能性を考察した.
|