2017 Fiscal Year Annual Research Report
Uniform computability verified in a mathematically strong system and semi-intuitionistic provability for existence sentences
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 |
本研究は,数学の定理の典型である存在定理「条件を満たす全てのXに対して,条件を満たす解Yが存在する」の解の計算とその証明に着目し,構成的数学,計算可能数学,逆数学を体系的に関連付けるものある. 昨年度の研究においては計算可能数学における存在定理「条件を満たす全てのXに対して,条件を満たす解Yが存在する」の証明可能性を「XからYを計算する(高階算術の意味で)原始再帰的な一様計算手続きが存在し,それが正しく解を与えていることが古典的な数学の大部分を展開するのに十分な逆数学の体系で証明できる」こととして形式化したが,計算可能解析学や計算可能組合せ論における具体的な存在定理の証明の解析を通して,その多くは再帰的ではあるが(高階算術の意味で)原始再帰的ではない一様計算手続きを与えるものであり,上記の形式化は計算可能数学における存在定理の証明可能性の表現としては弱すぎることが判明した. そこで,本年度は研究計画を見直し,計算可能数学における存在定理の証明可能性を逆数学に関連する形式体系を用いて形式化する方法について再検討した.そして,計算可能数学における存在定理の証明可能性の形式化の新しい候補を考え,それが言語を増やした準直観主義算術における証明可能性によって特徴付けられることを示した.しかし,その形式化の妥当性は依然として慎重に吟味されるべき問題であり,新しく与えた形式化が計算可能解析学や計算可能組合せ論における具体的な存在定理の証明にどの程度適応できるかを検証することは今後の課題である.
|
Research Progress Status |
29年度が最終年度であるため、記入しない。
|
Strategy for Future Research Activity |
29年度が最終年度であるため、記入しない。
|