| 研究課題/領域番号 |
18K13450
|
|---|
| 研究機関 | 早稲田大学 |
|---|
研究代表者 |
藤原 誠 早稲田大学, 高等研究所, 講師(任期付) (20779095)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2020-03-31
|
| キーワード | 相対的一様計算可能性 / 構成的数学 / 直観主義算術 / 存在定理 |
|---|
| 研究実績の概要 |
本年度は，まず，存在定理の間の相対的一様計算可能性と相対的構成的証明可能性の関係を考察するために，算術において2つの存在定理の間の相互一様計算可能性を適切に表現する形式化について具体例を鑑みつつ検討した．特に，計算可能組み合わせ論で考察されていた存在定理間の相互一様計算可能性や計算可能解析学で考察されていた存在定理間の相互一様計算可能性を注意深く観察し，有限型算術の枠組みの中でそれらを表現し得る形式化を考案した．これは自身が先行研究において与えた存在定理の一様計算可能性の形式化を拡張したものとなっている．
さらに，この形式化を用いて存在定理間の相互一様計算可能性を準直観主義算術における相互導出可能性によって特徴付けた．具体的には，比較的単純な論理式として形式化される2つの存在定理に対して，それら2つが相互一様計算可能でありかつその証明が非一様計算可能数学に対応する古典有限型算術で実行可能であることと，それら2つがおおよそ構成的数学に対応する準直観主義有限型算術において相互導出可能であることは同値であることを示した．さらに，比較的単純な論理式として形式化される2つの存在定理に対して，それら2つが相互一様計算可能性でありかつその証明が可述的数学に対応する古典有限型算術で実行可能であることと，それら2つが直観主義有限型算術にシグマ02二重否定シフト公理と可算選択公理を加えて得られる準直観主義有限型算術において相互導出可能であることは同値であることを示した．
これらにより，計算可能数学における存在定理の間の相対的一様計算可能性は，構成性の観点から古典論理を制限した弱い論理の上での相対的証明可能性を用いて部分的に特徴付けることができることが分かった．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
一様計算手続きを有限型算術の項を用いて表現するという自身が先行研究において提案した存在定理の一様計算可能性の形式化と同じ発想に基づき，2つの存在定理の間の相互一様計算可能性を有限型算術の枠組みの中で形式化し，その形式化を用いて存在定理の間の相対的一様計算可能性と相対的構成的証明可能性の関係を示すきれいなメタ定理を構築することに成功した．
このメタ定理は存在定理の構成的証明可能性と一様計算可能性の関係に関する自身の先行結果を相対化し拡張したものとなっている．
この成果により，計算可能数学における存在定理の間の相互一様計算可能性を構成的数学における構成性の観点から理解するための一つの試金石を与えることができた．
|
| 今後の研究の推進方策 |
これまでの研究により，既に存在定理の間の相対的一様計算可能性と相対的構成的証明可能性の関係を明らかに示すきれいなメタ定理が得られている．
今後は，計算可能数学において示されている相互一様計算可能な存在定理らをサンプルとして，得られているメタ定理が計算可能数学における具体的な結果に対してどの程度適用可能であるかを検証する．さらに，その検証結果を踏まえつつ，計算可能数学における存在定理の間の相互一様計算可能性を構成的数学における構成性の観点からどのように説明できるかについて考察する．
そして，これまでの研究によって得られているメタ定理を上記の考察と合わせて論文にまとめ，数学基礎論の国際論文誌に投稿する．
|
| 次年度使用額が生じた理由 |
2018年3月に予定していた海外の研究機関への研究訪問が先方との都合が合わずキャンセルとなったため．
|
