2012 Fiscal Year Research-status Report
| Project/Area Number |
23540130
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石原 哉 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (10211046)
|
|---|
| Keywords | 数学基礎論 / 数理論理学 / 構成的数学 / 逆数学 / 集合論 |
|---|
| Research Abstract |
構成的数学のための形式体系には、構成的的逆数学の体系EL0やMartin-Loefの型理論など型概念に基づく体系と、Aczelにより提案されたMartin-Loefの型理論に自然な解釈を持つ集合論Constructive Zermelo-Fraenkel set theory (CZF)など集合概念に基づく体系がある。本研究は、型理論に基づく体系EL0と集合論に基づく体系CZFにおける構成的逆数学の実践を通して、構成的逆数学のための集合概念に基づく形式体系を提案し、構成的逆数学のケーススタディを通した評価・改良を目的としている。
平成24年度は、前年度に明らかにした、単調完備定理で論理的公理（排中律）、算術的公理（帰納法）、関数の存在公理（選択公理）の役割を、EL0およびCZFにおいて精査した。その結果、単調完備定理に必要十分な排中律および帰納法が明確になったが、単調完備定理に必要十分な選択公理については、必要十分性を証明するには至っていない。これらの実践を通して、EL0における成果とCZFにおける成果との間の相互変換について精査し、EL0の保守的拡大となる集合論の体系Tを得るためには、CZFの公理の中でも外延性公理に対して、制限を加えらければならないことが明確になった。
さらに、集合概念に基づく体系の型理論に基づく体系での様々な解釈の調査を、前年度に引き続き行った。様々な解釈の中でもCZFをMartine-Loefの型理論へ自然に解釈する手法を応用し、体系TをEL0で解釈する手法に関して、考察を行った。
EL0の保守的拡大となる体系TではCZFの公理、特に外延性公理に対して、制約を加える必要があるため、体系Tで数学を自然に形式化することが難しい。そのため、数学を自然に形式化できる集合論の体系が自然に解釈できる、構成的逆数学のための型理論の体系を模索する研究を始めた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成24年度の研究実施計画に挙げた、構成的逆数学のための集合概念に基づく形式体系を、構成的数学の実践を通して、提案することを目指し、研究を行ってきた。研究はおおむね順調に進展している。
構成的数学の実践に関しては、型概念に基づく体系EL0と集合概念に基づく体系CZFにおいて、単調完備定理を精査し、その証明に必要十分な排中律と帰納法を明確にした。また、その証明に必要十分な選択公理に関しては、今後の研究課題として残っている。
また、これらの実践を通して、CZFの公理に加えるべき制限にを明らかにした。特に、外延性公理は、数学を自然に形式化するために重要であり、外延性公理を自然に解釈できるように、EL0をどのように拡張すればよいか解明を開始した。さらに、提案する集合論の体系TとEL0との保守的拡大性の証明に困難があるため、研究実施計画で挙げたように、体系EL0と体系Tの間の中間的な体系T'の模索し、それらの間の変換を導入しTの保守的拡大性を示す方針をとっている。
|
| Strategy for Future Research Activity |
今後も研究計画に沿って研究を推進する。特に、平成25年度は、構成的逆数学のための集合概念に基づく体系Tを確定するとともに、Tにおける構成的逆数学のケーススタディを通して、Tを評価し、改良する予定である。
構成的数学の実践としては、単調完備定理を引き続き、解析していく。特に、単調完備定理の証明に必要十分な選択公理が明確になっていないため、それを明らかにしてく予定である。
また、体系Tをさらに精査し、特に外延性公理の役割について明らかにしていく。外延性公理は、数学を自然に形式化するために重要であり、外延性公理を自然に解釈できる型概念に基づく体系を、EL0を拡張することにより、明らかにする予定である。さらに、体系Tと体系EL0の保守的拡大性を示すために、TとEL0の中間的な体系T'を明確にし、その間の変換を導入する予定である。
確定した体系T上で、位相空間の様々な構成的アプローチでのカテゴリー性、コンパクト性、一様性などに焦点を絞り、構成的逆数学のケーススタディを行う予定である。これを通して、体系Tの保守的拡大性を保ちながら、体系Tにどのような集合の公理を加えることができるかを明らかにする予定である。
|
| Expenditure Plans for the Next FY Research Funding |
今年度は、海外研究協力者訪問、研究成果発表等に研究費を使用した。また、国内外講師を招へいし講演を依頼する予定であったが、講師ならびに受け入れ側の都合が合わず、講師招へい旅費ならびに講演謝金を使用することがなかった。さらに、図書購入費は、他の予算で間に合ったため、使用することがなかった。これらの理由のため、次年度使用額が発生している。
次年度は、すでに国外講師4名～5名に講演を依頼しており、講演謝金が必要となる。また、洋書も前年度末にかけて発注していること、他の予算を期待することができないため、図書購入費が必要である。さらに、海外研究協力者訪問、研究成果発表等の旅費が必要である。このため、次年度使用額は次年度以降に請求する研究費と合わせて、旅費、講演謝金、図書購入費として、使用する予定である。
|
