並列タイトル等A study of sheaf models in constructive reverse mathematics
一般注記本研究は、(1)構成的逆数学における未解決問題の解決と新たな公理の発見、（２）層モデルを用いた公理や定理の体系的な分離手法の構築、（３）分離手法などメタ理論の構成的数学の枠組みでの展開を目的とする。（１）単調完備定理と同値になる原理、有界内包公理、を明らかにした。2進展開定理と中間値の定理と同値になる弱いケーニッヒの補題に対する条件を解明した。（２）2つの順序構造とその間の単調写像により構成される、拡張フレームの概念を提案した。拡張フレーム上のクリプキ層モデルを用いて、様々な公理を体系的に分離する手法を開発した。（３）上記クリプキ層モデルの構成が構成的集合論の枠組みで展開できることを示した。 研究成果の学術的意義や社会的意義： 構成的逆数学は、様々な哲学のもとに展開された数学を、統一的な視点から論理的公理および関数（集合）の存在公理などにより分類・整理・体系化するという斬新で独創的な研究である。本研究により、構成的逆数学の重要な未解決問題を解決し、新たな公理を発見し、公理（定理）の体系的な分離手法を構築することにより、排中律などの論理的公理、可算選択公理などの関数の存在公理、および新たに発見された公理のなす束構造の解明と解析が大きく進展した。直観主義論理では証明とプログラムの間に自然な対応がある。直観主義論理の証明からプログラムを抽出し高信頼ソフトウェアを開発するための基盤理論の深化や限界の解明に寄与した。：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.
基盤研究(C)（一般）
研究期間：2016～2018
課題番号：16K05251
研究者番号：10211046
研究分野： 数理論理学・構成的数学
identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/16038
一次資料へのリンクURLhttps://dspace.jaist.ac.jp/dspace/bitstream/10119/16038/1/16K05251seika.pdf
連携機関・データベース国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）
提供元機関・データベース北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ