| Project/Area Number |
16K05251
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Foundations of mathematics/Applied mathematics
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
ISHIHARA Hajime 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (10211046)
|
|---|
| Research Collaborator |
Nemoto Takako
Yokoyama Keita
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Project Status |
Completed (Fiscal Year 2018)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2018: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2017: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
Fiscal Year 2016: ¥1,560,000 (Direct Cost: ¥1,200,000、Indirect Cost: ¥360,000)
|
|---|
| Keywords | 構成的数学 / 逆数学 / 層モデル / 数学基礎論 |
|---|
| Outline of Final Research Achievements |
This research aims at (1) solving open problems and finding new axioms in constructive reverse mathematics, (2) developing a systematic method to separate axioms and theorems using sheaf models, (3) developping the systematic method in constructive mathematics.
(1) We showed that the monotone convergence theorem is equivalent to a restricted bounded comprehension axiom, and showed that the binary expansion theorem and the intermediate value theorem are equivalent to restricted versions of the weak Koenig lemma. (2) We propose the notion of an extended frame consisting of two partially ordered sets and a monotone mapping between them, and develop a systematic method to separate axioms and theorems using Kripke sheaf models over extended frames. (3) We showed that the construction of a Kripke sheaf model over an extended frame is done within the framework of constructive set theory.
|
| Academic Significance and Societal Importance of the Research Achievements |
構成的逆数学は、様々な哲学のもとに展開された数学を、統一的な視点から論理的公理および関数（集合）の存在公理などにより分類・整理・体系化するという斬新で独創的な研究である。本研究により、構成的逆数学の重要な未解決問題を解決し、新たな公理を発見し、公理（定理）の体系的な分離手法を構築することにより、排中律などの論理的公理、可算選択公理などの関数の存在公理、および新たに発見された公理のなす束構造の解明と解析が大きく進展した。
直観主義論理では証明とプログラムの間に自然な対応がある。直観主義論理の証明からプログラムを抽出し高信頼ソフトウェアを開発するための基盤理論の深化や限界の解明に寄与した。
|
