2016 Fiscal Year Annual Research Report
構成的数学・計算可能数学・逆数学の接合点：存在定理の解の計算とその証明
| Project/Area Number |
16H07289
|
|---|
| Research Institution | Waseda University |
|---|
Principal Investigator |
藤原 誠 早稲田大学, 高等研究所, 助教 (20779095)
|
|---|
| Project Period (FY) |
2016-08-26 – 2018-03-31
|
| Keywords | 逆数学 / 構成的数学 / 計算可能数学 / 存在定理 |
|---|
| Outline of Annual Research Achievements |
構成的数学，計算可能数学，逆数学は1960年代以降大きく発展した数学基礎論の主要分野であり，それぞれ「構成可能性」「計算可能性」「必要十分な公理系」という観点から数学の諸定理を解析する．本研究の目的は，数学の定理の典型である存在定理「条件を満たす全てのXに対して，条件を満たす解Yが存在する」の解の計算とその証明に着目し，それら3分野を体系的に関連付けることである．具体的には，一般の存在定理に対する「構成的数学における証明可能性」及び「解の一様計算可能性」を逆数学の体系を用いて形式化し，構成的数学における証明可能性が計算可能数学における解の一様計算可能性よりも真に厳しいことを実証することが最終的な目標となる．
本年度筆者は，存在定理「条件を満たす全てのXに対して，条件を満たす解Yが存在する」の解の一様計算可能性を「XからYを計算する原始再帰的な一様計算手続きが存在し，それが正しく解を与えていることが古典的な数学の大部分を展開するのに十分な逆数学の体系で証明できる」こととして形式化し，比較的単純な論理式として形式化される全ての存在定理に対して，その解の一様計算可能性はシグマ02二重否定シフト原理を含む準直観主義算術体系における証明可能性によって特徴づけられることを示した．このために，否定翻訳と呼ばれる証明論の手法や(型付き)実現可能解釈と呼ばれる証明論の手法を駆使した．構成的数学における証明の大部分は直観主義算術の上で形式化できることが知られているが，直観主義算術では証明できない二重否定シフト原理(の非常に弱い断片)が存在定理の解の一様計算可能性を特徴付けることを明らかにしたことがこの研究成果の特筆すべき点である．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
先行研究により，シグマ02二重否定シフト原理は直観主義算術では証明できないことが知られていた．一方，筆者は本研究課題の成果として，比較的単純な論理式として形式化される全ての存在定理の算術的内包公理ACAを含む算術体系における一様計算可能性は，シグマ02二重否定シフト原理を含む準直観主義算術体系における証明可能性によって特徴づけられることを示した．これは「構成的数学における証明可能性」が「計算可能数学における解の一様計算可能性」よりも真に厳しいことを示す一つのメタ数学的な結果が得られたことを意味するものであり，構成的数学と計算可能数学を繋ぐ新たなる架け橋となるものである．
|
| Strategy for Future Research Activity |
今後は，まず計算可能解析学や計算可能組合せ論における具体的な存在定理の証明を注意深く分析し，解の一様な計算手続きを与えてはいるが，その証明に算術的集合存在公理ACAを本質的に使用している存在定理を見つける．さらに，構成的逆数学の手法及び直観主義算術における論理原理の階層構造を利用して，その存在定理がシグマ02二重否定シフト原理を含まない直観主義算術体系では証明不可能であることを示すことを目指す．これが達成されれば，これまでの研究成果と合わせて，「構成的数学における証明可能性」が「計算可能数学における解の一様計算可能性」よりも真に厳しいことを基礎付けるメタ定理及びその具体例の両方が得られたことになる．
|
