2023 Fiscal Year Research-status Report
Constructive reverse mathematics and its framework
| Project/Area Number |
23K03205
|
|---|
| Research Institution | Tokyo University of Science |
|---|
Principal Investigator |
藤原 誠 東京理科大学, 理学部第一部応用数学科, 助教 (20779095)
|
|---|
| Project Period (FY) |
2023-04-01 – 2028-03-31
|
| Keywords | 逆数学 / 構成的数学 / 直観主義数学 / 直観主義論理 / 冠頭標準形 |
|---|
| Outline of Annual Research Achievements |
本研究は構成的逆数学の方法論を用いて既存の数学や直観主義数学を現代的立場から再考察するものであり，具体的な研究課題は「A. 直観主義数学における公理や定理に対する構成的逆数学」，「B. 直観主義数学を計算可能解析学や古典的逆数学と関連づけるメタ定理の開発」，「C. 構成的逆数学の枠組みの見直しと整備」に大別される．
課題Aに関し，可算関数存在公理を許容する直観主義数学や従来の構成的数学では同値となるが，弱い関数存在公理しか持たない構成的逆数学の基礎体系では同値とならない一般の決定可能ファン定理と完全二分岐木に対する決定可能ファン定理の差について詳しく解析し，根元多佳子氏(東北大学)との共同研究の成果として，その差を埋める関数存在公理を特定した．
課題Bに関しては，計算可能解析学と逆数学の直接的な関係を解析するための新たなるメタ定理の開発に取り組んでいる最中であるが，現時点で有用なメタ定理を構築するための着想が既に得られている．
課題Cに関しては，証明論的手法を構成的逆数学に応用するための基礎研究として，一階述語論理式のクラス分けについての研究を行った．特に，倉橋太志氏(神戸大学)との共同研究により，半直観主義算術における冠頭標準形定理のために2004年の先行研究において導入されていた論理式のクラスが通常の冠頭標準変換によってΣ_kやΠ_kと言われる論理式に変形されるクラスとちょうど一致していることを明らかにした．この結果は半直観主義算術における冠頭標準形定理の妥当性を保証するものである．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究における具体的な各課題に対してそれぞれ一定の成果が得られているため．
|
| Strategy for Future Research Activity |
直観主義数学における公理や定理に対する構成的逆数学に関して，これまでの研究及び調査により，ケーニヒの補題や弱ケーニヒの補題に関する一部の公理の証明には原始再帰法が不可欠であることが分かってきた．ケーニヒの補題や弱ケーニヒの補題，決定可能ファン定理についてはこれまでいくつもの重要な構成的逆数学研究が行われているが，今後はそれらを原始再帰法を制限した立場から再検討し，ケーニヒの補題や弱ケーニヒの補題，決定可能ファン定理に関するより精密な構成的逆数学を展開する．
また，前年度から取り組んでいる計算可能解析学と逆数学の直接的な関係を解析するための新たなるメタ定理の開発に継続して取り組む．特に，Weihrauch還元可能性のverificationに必要な公理系の強さを測るためのメタ定理の構築を目指す．
さらに，証明論的手法を構成的逆数学に応用するための基礎研究として，直観主義論理や半直観主義論理に基づく理論においてΣ_kやΠ_kと言われる証明論的に扱いやすい形の論理式に変形される論理式の階層的クラスを構築することを目指す．
|
| Causes of Carryover |
双方の都合により，研究打ち合わせのための国内出張の期間を当初の予定よりも短縮せざるを得ず，出張旅費が予定額よりも低くなったために次年度使用額が生じた．その分昨年度は研究打ち合わせを十分に行うことができなかったため，今年度は研究打ち合わせのための国内出張期間を長く取る予定である．次年度使用額はそのための経費に充当する．
|
Research Products
(6 results)
