2022 Fiscal Year Research-status Report
Constructive reverse mathematics and computational content of mathematical theorems
| Project/Area Number |
21KK0045
|
|---|
| Research Institution | Japan Advanced Institute of Science and Technology |
|---|
Principal Investigator |
石原 哉 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (10211046)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
河井 達治 高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
横山 啓太 東北大学, 理学研究科, 教授 (10534430)
根元 多佳子 広島工業大学, 環境学部, 准教授 (20546155)
藤原 誠 東京理科大学, 理学部第一部応用数学科, 助教 (20779095)
|
|---|
| Project Period (FY) |
2021-10-07 – 2026-03-31
|
| Keywords | 構成的逆数学 / 直観主義算術 / 論理公理の階層 / 超算術的公理 |
|---|
| Outline of Annual Research Achievements |
「様々な公理の解析」の主な成果は、唯一解をもつ弱ケーニヒの補題を構成的逆数学の観点から解析し、同主張が2つの論理公理と2つの関数存在公理に分離できることを示した。また、有限分木のheight-wise bounding function の存在の選択公理と帰納法による特徴づけを行った。さらに、構成的逆数学のための枠組み研究として、直観主義算術上の論理公理の階層構造の関係を詳しく解析し、その構造を明らかにした。「算術における逆数学」では、リーズ大学の研究者との共同研究により算術において強い公理を要請する解析学の命題の探索を進めている。最近の共同研究で超算術的公理系に対応する初等的命題も見つかった。また、「Cantor区間上の実連続関数が連続なモジュラスを持つ」という主張(命題)を構成的逆数学の観点から考察した。「集合論における逆数学」では、局所的コンパクト空間の位相のpoint-free位相表現を与えた。また、実数の集合（有理数の集合の完備化）は、有理数の基本列の集合とその上の同値関係で与えられる。古典的集合論では、基本列の集合を同値関係で割った商集合として実数の集合を定義する。商集合として定義すると、個々の基本列（代表元）の情報が失われ、それを取り出すためにはフルの選択公理が必要であり構成性が壊れてしまう。この状況を回避するために構成的集合論では実数全体を集合としてではなくセトイド（集合とその上の同値関係の対）として定義する必要があることが判明した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
「様々な公理の解析」では、有限分木とケーニッヒの補題についての研究が順調に進展し、当初の予想よりも良い形で特徴づけられ顕著な結果が得られている。また、今後の課題も明らかになった。一方、新型コロナ・ウイルスの感染拡大により海外の研究拠点を直接訪問することが難しく、その影響もあって未だ国際共同研究の開始には至っていない。「算術における逆数学」では、これまで継続して研究を進めてきたカリスティの不動点定理についての逆数学分析が完了・論文も受理され、新たな研究テーマとしてより強い算術体系を完備距離空間の性質で特徴付けるためのアイデアの萌芽も得ている。また、「Cantor区間上の実連続関数が連続なモジュラスを持つ」という主張を構成的逆数学の観点から考察し、WKLとQF-ACの仮定の下で成り立つことを示した。同様の結果はBishopの構成的数学では知られていたが、本結果では選択公理をQF-ACに制限した条件で示すことに成功した点が重要である。「集合論における逆数学」では、構成的位相空間論において、従来の局所的コンパクトハウスドルフ空間の有限なpoint-free位相表現を与えた。
|
| Strategy for Future Research Activity |
古典的逆数学では、ケーニッヒの補題の特徴づけは集合内包公理ACAで与えられるが、今回の研究では構成的逆数学では論理原理LLPO＋複数の種類の選択公理という形で与えられた。今後の研究では、ACAとの関係も明らかにすることで、古典的逆数学の結果を拡張する。2023年度中にルートヴィッヒ・マキシミリアン大学ミュンヘンの研究グループを直接訪問し、自身の最新の研究成果について報告すると共に、「様々な公理の解析」および「プログラム理論の構築」に関する共同研究の構想を練るための研究打ち合わせを行う。これまで十分には行えなかった相互訪問による対面での議論を充実させること共同研究の加速をはかる。「算術における逆数学」では、これまでの研究で得られたクリプキモデルの直観主義/古典算術の翻訳手法への適用のアイデアの実現を目指す。構成的逆数学に関しては、命題「Cantor区間上の実連続関数が連続なモジュラスを持つ」が古典数学の基礎体系RCA0で証明できるか、また、BDNやWMPなどの非常に弱い非構成的原理の基で成り立つかとう問題に取り組む予定である。上記命題は弱いACを含むと予想されることから、今後の研究では弱いACを分離できモデルの構成を目指す。「集合論における逆数学」では、セトイドを自然に扱うための枠組みの構築を行う。
|
| Causes of Carryover |
コロナ禍の影響で予定していた海外渡航が十分にできず、また予定していた金沢でのワークショップも開催を延期したため。次年度より日本の水際対策が大幅に緩和されるため、コロナ禍以前と同様に海外渡航を再開する予定である。
|
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
[Book] 証明作法2023
Author(s)
石原 哉
Total Pages
232
Publisher
共立出版
ISBN
9784320114890
