2011 Fiscal Year Research-status Report
| Project/Area Number |
23540130
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (10211046)
|
|---|
| Project Period (FY) |
2011-04-28 – 2014-03-31
|
| Keywords | 数学基礎論 / 数理論理学 / 構成的数学 / 逆数学 / 集合論 |
|---|
| Research Abstract |
構成的数学のための形式体系には、構成的逆数学の体系EL0やMartin-Loefの型理論など型概念に基づく体系と、集合概念に基づく体系がある。Aczelは、Martin-Loefの型理論に自然な解釈を持つ集合論CZFを提案した。本研究は、体系EL0とCZFにおける構成的逆数学の実践を通して、構成的逆数学のための集合概念に基づく形式体系を提案し、構成的逆数学のケーススタディを通した評価・改良を目的としている。 平成23年度は、EL0において単調完備定理を考察し、同定理において排中律、帰納法、選択公理それぞれが果たす役割を明らかにした。また、CZFにおいて、集合生成であるクラスの特徴づけを行った。これらの実践を通して、EL0における成果とCZFにおける成果との間の相互変換について考察し、EL0の保守的拡大となる集合論の体系Tを得るためには、CZFの公理にかなりの制約を加えなければならないことが明らかになった。 さらに、集合概念に基づく体系の型理論に基づく体系での様々な解釈の調査を行った。その結果、CZFをMartin-Loefの型理論への自然に解釈する手法は強力であり、体系TをEL0で解釈する際にも応用できることが明らかになった。 EL0の保守的拡大となる体系TではCZFの公理に多くの制約を加える必要があるため、体系Tで数学を自然に形式化することが難しくなる。そのため、むしろEL0を拡張し、数学を自然に形式化できる集合論の体系が自然に解釈できる、構成的逆数学の体系を見出す研究も必要である。また、構成的逆数学の体系と集合論の体系の間の中間的な体系を考え、それらの間の解釈を与えることにより、より自然な解釈が構成できる見通しを得た。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成23年度の研究実施計画に挙げた、構成的逆数学における問題の体系EL0と体系CZFにおける解決、集合概念に基づく体系の型概念に基づく体系での解釈手法の調査は、順調に進展している。 EL0において単調完備定理を考察し、同定理において排中律、帰納法、選択公理それぞれが果たす役割が明らかになった。また、CZFにおいて、集合生成であるクラスを特徴づけることができた。これらの実践を通して、EL0における成果とCZFにおける成果との間の相互変換について考察ができた。さらなる問題の解決を試み、それを通してさらなる知見を得る必要がある。また、EL0の保守的拡大となる集合論の体系Tを得るためには、CZFの公理にかなりの制約を加えなければならないことを明らかにした。 さらに、集合概念に基づく体系の型理論に基づく体系での様々な解釈の調査も順調に進展した。CZFのMartin-Loefの型理論への自然な解釈の手法の解析も終わっている。その結果、CZFをMartin-Loefの型理論への自然に解釈する手法は強力であり、体系TをEL0で解釈する際にも応用できることが明らかになっている。
|
| Strategy for Future Research Activity |
今後も研究実施計画に沿って研究を推進する。特に、平成24年度は、構成的逆数学のための集合概念に基づく体系の提案を行う予定である。 集合論の体系CZFの公理に制限を加えることにより、構成的逆数学のための集合論の体系Tを提案する。体系Tの命題AからEL0の命題f(A)への解釈fを定義し、f(A)がEL0で証明可能であることと、Aが体系Tで証明可能であることの同値性、およびf(A)とAがEL0で同値であることを示し、保守的拡大性を証明する予定である。解釈fを与える際に、より自然な解釈を与えるために、体系TとEL0の間の中間的な体系を構築し、それらの間の解釈を導入する予定である。 また、構成的逆数学における問題の解決も引き続き行い、その実践を通してEL0における成果と集合論の体系CZFにおける成果との相互変換について考察を継続する。 さらに、提案した体系Tの構成的数卓のケーススタディを通した評価・改良を行う予定である。提案した体系T上で、位相空間の様々な構成的アプローチでのカテゴリー性、コンパクト性、一様性などに焦点を絞り、構成的逆数学のケーススタディを行う予定である。これを通して、体系Tの保守的拡大性を保ちながら、体系Tにどのような集合の公理を加えることができるかを明らかにする予定である。
|
| Expenditure Plans for the Next FY Research Funding |
今年度は、海外研究協力者訪問、研究成果発表、国内研究者の招へい等に研究費を使用した。また、国内外講師を招へいし講演を依頼する予定であったが、講師ならびに受け入れ側の都合が合わず、講師招へい旅費ならびに講演謝金を使うことがなかった。さらに、図書購入費は、他の予算で間に合ったため、使用することがなかった。これらの理由のため、次年度使用額が発生している。 次年度は、海外研究協力者訪問、研究成果発表などの旅費に加え、多くの国内外の講師を招へいし講演を依頼するための旅費および講演謝金が必要となる。また、図書購入費も、他の予算を期待することはできない。このため、次年度使用額は次年度以降に請求する研究費と合わせて、旅費・講演謝金・図書購入費等として、使用する予定である。
|
