|
構成的数学のための形式体系には、EL0やMartin-Loefの型理論など型概念に基づく体系と、Aczelにより提案されたMartin-Loefの型理論に自然な解釈をもつ集合論 Constructive Zermelo-Fraenkel set theory（CZF）など集合概念に基づく体系がある。本研究は、型概念に基づく体系EL0と集合論に基づく体系CZFにおける構成的逆数学の実践を通して、構成的逆数学のための集合概念に基づく形式体系を提案し、構成的逆数学のケーススタディを通した評価・改良を行い、構成的逆数学において高度に抽象的な対象を自然に扱えるようにすることである。
平成25年度は、前年度までの単調完備定理を中心とした定理のEL0およびCZFでの逆数学の実践、それを通したEL0およびCZFとの間の相互変換の精査、集合概念に基づく体系の型理論に基づく体系での様々な解釈の調査などを踏まえて研究を行った。その結果、次の研究成果・知見を得た。（１）CZFの外延性公理をEL0で解釈することに非常な困難がともなうため、まず外延性公理のあるCZFを外延性公理のない集合論で解釈し、さらに外延性公理のない集合論をEL0で解釈するように２段階に分けた。（２）CZFを直接EL0で解釈することに困難がともなうため、中間的な体系としてEL0に自然な解釈を持つ演算理論体系APPを考え、CZFをAPPで直接的に解釈する手法を提案した。（３）CZFをAPPで直接的に解釈するほかにAPPにおけるCZFの実現可能性解釈の調査を行った。
今後の研究課題としては、CZFのAPPにおける直接的な解釈と実現可能性解釈で（CZFの公理に限定することなく）どのような集合の存在公理が解釈できるか解明することが残った。
|
