| Project/Area Number |
22K03401
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 12030:Basic mathematics-related
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
木原 貴行 名古屋大学, 情報学研究科, 准教授 (80722701)
|
|---|
| Project Period (FY) |
2022-04-01 – 2026-03-31
|
| Project Status |
Granted (Fiscal Year 2022)
|
| Budget Amount *help |
¥4,160,000 (Direct Cost: ¥3,200,000、Indirect Cost: ¥960,000)
Fiscal Year 2025: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2024: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2023: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2022: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
|
|---|
| Keywords | 実現可能性トポス / Lawvere-Tierney位相 / Weihrauch次数 / チューリング次数 / 構成的数学 / 構成的逆数学 / 幾何様相 / エフェクティブ・トポス |
|---|
| Outline of Research at the Start |
数学基礎論において，数学の定理を示すための必要最小限の公理を探る逆数学と呼ばれるプロジェクトがある．本研究課題では，逆数学に対して，トポス理論の概念である幾何様相(Lawvere-Tierney位相)を用いた新たなアプローチを行う．その根幹は《相対実現可能性トポス上の幾何様相全体のなす内的フレーム構造の分析は，一種の逆数学だと思える》という発見に基づく．
|
| Outline of Annual Research Achievements |
本年度は，計算論における神託概念がLawvere-Tierney位相とみなせるという観点を詳細に突き詰め，神託概念と真理値上の演算に関する多数の結果を得た．LT-位相の概念は，内的単調性，増強性，冪等性の3つの性質によって特徴付けられる．計算論における万能マシンの性質を抽象化することによって，内的単調性と関連する性質が現れることを明らかにし，内的単調性とWeihrauch還元可能性の関連性を明らかにした．同様の方法で，これに増強性を付加したものが点付きWeihrauch還元可能性，さらに冪等性を加えると一般Weihrauch還元可能性に対応することも明らかにした．また，LT-位相は部分トポスと対応することが知られているが，そのうち実効トポスの実現可能性部分トポスに対応する神託概念はSasso流のサブチューリング還元と対応することを明かした．
サブチューリング次数については，シンガポール南洋理工大学のKeng Meng Ng氏と共同研究を進め，サブチューリング次数（したがって実効トポスの実現可能性部分トポス）が非分配的な束をなし，結び既約次数を持ち，極小対が存在しない，など数々の次数論的性質を証明した．その中で，特に擬極小サブチューリング次数に関する様々な結果を得て，これを応用して，形式チャーチ提唱(CT)と拡張形式チャーチ提唱(ECT)を分離する最初のモデルの構築に成功し，構成的逆数学への様々な応用を示した．
|
| Current Status of Research Progress |
Current Status of Research Progress
1: Research has progressed more than it was originally planned.
Reason
神託計算とLawvere-Tierney位相の詳細な分析が順調に進み，その結果として，LT-位相の3つの性質がそれぞれ計算論的に自然な意味を持つことが明らかになった．そして，実効トポスの実現可能性部分トポスに対応するLT-位相の計算論的対応物はSasso流サブチューリング次数となるが，この分析が想像以上に進展し，その非分配性証明や結び既約次数の存在等の数多くの非自明な結果を得るに至った．特に擬極小次数に関する結果を構成的数学のモデルの構成へと応用することに成功し，形式チャーチ提唱(CT)と拡張形式チャーチ提唱(ECT)の分離に成功したのは，想定外の結果であった．
|
| Strategy for Future Research Activity |
実効トポスの実現可能性部分トポスに対応する次数概念であるSasso流サブチューリング次数について，既に数多くの結果が得られているものの，まだ数多くの問題が残されているため，その研究を進める予定である．また，構成的数学の応用であるが，形式チャーチ提唱には様々な変種があるので，全パターンの組合せを分離する構成的数学のモデルを構成するのが今後の目標である．また，形式チャーチ提唱以外の他の重要な構成的原理についても分析を進めていく．
|
Report
(1 results)
Research Products
(14 results)
