|
申請首はこれまで直観主義的手法を用いた、これまでの形式的なものよりもわかりやすい証明論を開発してきた。論理学的課題としては、スタンフォード大学G.ミンツ教授との共同研究を押し進める点があげられていた。今年度は、共同研究を押し進めた結果、ブフホルツのΩ規則をさらに拡張することに成功した。1970年代終わりにΩ規則が導入されて以来、Ω規則を含む体系に対するカット消去定理は常に部分的なものであった。つまり、算術的と呼ばれる限定されたクラスの論理式を帰結としてもつ証明図に関するカット消去定理のみが証明されていた。それに対して、本研究では、Ω規則を含む体系に対するカット消去定理を「任意の」論理式を帰結としてもつ証明図へと拡張することができた。共同研究では、この手法が繰り返しを含まない再帰的定義に対応する二階算術の部分体系に対して適用され、成果をG.ミンツ教授との共同研究としてまとめ査読付きの国際誌へと投稿した。その後、この手法をω回の繰り返しを含む再帰的定義に対応する二階算術の部分体系へと拡張することに成功し単著論文にまとめ投稿の準備を進めている。これらの研究のため、スタンフォード大学を訪問し共同討議を行った。
哲学的課題については、まず準備段階として申請者が開発してきた証明論がどのような体系で形式化されるかを探求した。その結果、やはり形式主義的枠組みを超えた原理を使っていることが明らかになった。さらにゲンツェンの1936年の無矛盾性証明が現代的証明論のテクニックを用いて再構成できることが判明し論文にまとめた。
|
