存在定理の一様証明可能性及び直観主義証明可能性に関する逆数学的解析

今年度は本研究課題に関して大きく二つの成果が得られた．まず，直観主義高階算術における論理原理の織り成す構造の解析において，重要な研究成果が得られた．特に，古典的逆数学における観点から自然に考えられる12種類の論理原理を検討し，それらの論理原理とマルコフ原理等これまで構成的逆数学で扱われてきた3種類の論理原理との逆数学的関係性を完全に解明した．マルコフ原理よりも弱い論理原理はこれまでにほとんど発見されておらず，本研究成果は構成的逆数学に一つの新たなる階層をもたらすものとなった．なお，本研究成果は北陸先端科学技術大学院大学の石原哉教授，根元多佳子助教との共同研究の成果である．この研究の延長として，自然に考えられる他の論理原理についても現在調査を進めている．一方で，存在定理の一様証明可能性及び直観主義証明可能性に関する新たなるメタ定理が得られた．自身の先行結果のさらなる拡張として，比較的単純な形のΠ12論理式として形式化される全ての存在定理Sに対して，「Sが弱ケーニヒの補題WKLを含む古典的逆数学の体系で一様証明可能であること」と「Sが構成的数学の体系で証明可能であること」が同値であることを示した．この証明にはmonotone functional interpretationと呼ばれるProof mining研究で用いられている証明論の手法を使った．

今年度は本研究課題に関して大きく二つの成果が得られた．まず，直観主義高階算術における論理原理の織り成す構造の解析において，重要な研究成果が得られた．特に，古典的逆数学における観点から自然に考えられる12種類の論理原理を検討し，それらの論理原理とマルコフ原理等これまで構成的逆数学で扱われてきた3種類の論理原理との逆数学的関係性を完全に解明した．マルコフ原理よりも弱い論理原理はこれまでにほとんど発見されておらず，本研究成果は構成的逆数学に一つの新たなる階層をもたらすものとなった．なお，本研究成果は北陸先端科学技術大学院大学の石原哉教授，根元多佳子助教との共同研究の成果である．この研究の延長として，自然に考えられる他の論理原理についても現在調査を進めている．一方で，存在定理の一様証明可能性及び直観主義証明可能性に関する新たなるメタ定理が得られた．自身の先行結果のさらなる拡張として，比較的単純な形のΠ12論理式として形式化される全ての存在定理Sに対して，「Sが弱ケーニヒの補題WKLを含む古典的逆数学の体系で一様証明可能であること」と「Sが構成的数学の体系で証明可能であること」が同値であることを示した．この証明にはmonotone functional interpretationと呼ばれるProof mining研究で用いられている証明論の手法を使った．