研究課題
本研究は，数学の定理の典型である存在定理「条件を満たす全てのXに対して，条件を満たす解Yが存在する」の解の計算とその証明に着目し，構成的数学，計算可能数学，逆数学を体系的に関連付けるものある．昨年度の研究においては計算可能数学における存在定理「条件を満たす全てのXに対して，条件を満たす解Yが存在する」の証明可能性を「XからYを計算する(高階算術の意味で)原始再帰的な一様計算手続きが存在し，それが正しく解を与えていることが古典的な数学の大部分を展開するのに十分な逆数学の体系で証明できる」こととして形式化したが，計算可能解析学や計算可能組合せ論における具体的な存在定理の証明の解析を通して，その多くは再帰的ではあるが(高階算術の意味で)原始再帰的ではない一様計算手続きを与えるものであり，上記の形式化は計算可能数学における存在定理の証明可能性の表現としては弱すぎることが判明した．そこで，本年度は研究計画を見直し，計算可能数学における存在定理の証明可能性を逆数学に関連する形式体系を用いて形式化する方法について再検討した．そして，計算可能数学における存在定理の証明可能性の形式化の新しい候補を考え，それが言語を増やした準直観主義算術における証明可能性によって特徴付けられることを示した．しかし，その形式化の妥当性は依然として慎重に吟味されるべき問題であり，新しく与えた形式化が計算可能解析学や計算可能組合せ論における具体的な存在定理の証明にどの程度適応できるかを検証することは今後の課題である．
29年度が最終年度であるため、記入しない。
すべて 2017
すべて 雑誌論文 (1件) (うち査読あり 1件)
The Bulletin of Symbolic Logic
巻: vol. 23, no.2 ページ: 241-242
