2018 Fiscal Year Annual Research Report
A study of sheaf models in constructive reverse mathematics
| Project/Area Number |
16K05251
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石原 哉 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (10211046)
|
|---|
| Project Period (FY) |
2016-04-01 – 2019-03-31
|
| Keywords | 構成的数学 / 逆数学 / 層モデル |
|---|
| Outline of Annual Research Achievements |
本研究は、１．構成的逆数学における未解決問題の解決と新たな公理の発見、２．層モデルを用いた公理や定理の体系的な分離手法の構築、３．分離手法などメタ理論の構成的数学の枠組みでの展開を目的とする。
これにより、論理的公理・関数の存在公理および新たに発見された公理のなす束構造の解明と解析が大きく進展する。また、本研究では様々な公理を層モデルの性質により特徴づけ解析することにより、研究をより高次な視点から深化させる。メタ理論を構成的数学の枠組みで展開し実証することにより、研究に数学的・技術的な貢献以上の意味・意義を与える。
平成３０年度は、研究の進展が遅れていた２．に焦点をあて研究をおこなった。クリプキ層モデルを用いて公理や定理の体系的な分離手法の構築を目指した。クリプキ層モデルはフレームと呼ばれる順序構造の上に構築されるが、公理や定理を体系的に分離するためには単に順序構造のみでは不十分であることが分かった。そのため、２つの順序構造とその間の単調写像により構成される、拡張フレームの概念を提案した。拡張フレームを用いることにより、命題論理における様々な公理を体系的に分離できることを、排中律（PEM）、２重否定除去（DNE）、弱い排中律（WPEM）、ド・モルガンの法則（DML）、弱いド・モルガンの法則（WDML）、制限された排中律（RPEM）などを例に示した。また、拡張フレーム上のクリプキ層モデルを用いて、述語論理における様々な公理を分離する手法を開発した。これにより、上記命題論理の公理を含め、命題論理式に存在命題を代入して得られる公理が体系的に分離できることを示した。さらに、その手法を１階算術体系に適用し算術体系においてなどの様々な公理を分離するための体系的な手法を開発した。３．に関連して、上記分離手法のうち述語論理までの部分は１点を除き、構成的集合論の枠組みで展開できることを確認した。
|
