| 研究実績の概要 |
前年度の研究の中で派生・発展した有限組み合わせ論の手法を証明の長さの分析に応用する研究について、共同研究者の L. Kolodziejczyk 博士, T. L. Wong 博士を日本に招聘して集中して議論を行うことで完遂し、結果を論文にまとめた。最も重要な成果は無限組み合わせ命題の利用により有限組み合わせ命題の証明の長さがどれだけ短縮しうるかを明らかにしたことである。また併せて、諸種の証明体系の間で証明の長さを比較するより汎用的な手法も得ることが出来、これにより採集原理と帰納法公理の証明の長さの比較に関するParisの問題も解決された。
また、上述の課題から得られた算術のモデル論的手法が、RCA_0*と呼ばれる非常に弱い証明体系での組み合わせ命題の分類問題にも応用できることも発見し、ワルシャワ・シンガポールの研究グループと連携してさらなる研究を続けている。
以上により、本研究課題の最重要テーマであった「多重視点に対応した証明解析手法の融合、およびそれを基にしたラムゼイの定理や関連組み合わせ命題の評価」が完了した。既に前年度までに完了していた「算術・逆数学手法の応用により計算機の停止性検証アルゴリズムの理論的限界を求める手法の構築」「解析学の逆数学分野の新たな現象の解明」と合わせて本研究課題で挙げていた主要な研究テーマは全て解決された。また各テーマはそれぞれ新たな研究テーマを生み出しており、上述の弱い証明体系への応用等、既にいくつかの重要な進展を得ている。
|
