2023 Fiscal Year Research-status Report
Computability theory on intuitionistic logic and its application to constructive reverse mathematics
| Project/Area Number |
18K03392
|
|---|
| Research Institution | Tohoku University |
|---|
Principal Investigator |
根元 多佳子 東北大学, 情報科学研究科, 准教授 (20546155)
|
|---|
| Project Period (FY) |
2018-04-01 – 2025-03-31
|
| Keywords | 構成的数学 / 逆数学 / 証明論 / 再帰理論 |
|---|
| Outline of Annual Research Achievements |
2023年度の研究実績としては、(1)構成的逆数学における公理WKL!!の論理原理と選択公理による特徴づけについての論文(2)構成的集合論におけるrealizability interpretationを用いた様々な集合論のモデルの構築についての論文(3)直観主義算術上のクリプキモデルによる非構成的論理原理の統一的な手法による分離法を示した論文の計３本が出版され、(4)構成的逆数学におけるケーニッヒの補題と弱ケーニッヒの間を補完する原理の特徴づけに関する論文が受理された。この他(5)構成的逆数学のための各種の形式体系と一階算術の体系との関係、および古典論理上の二階算術の体系との関係について解説した記事が収録した書籍Handbook of Constructive Mathematicsが出版された。また、構成的逆数学の最近の研究結果について、(1)公理WKL!!の特徴づけについて(2)公理WKLと論理原理、帰納法原理の関係について(3)最近の構成的数学の研究の動向について国際学会における招待講演を計3件行った。
この他の研究成果としては、構成的逆数学における\Sigma^0_1帰納法とケーニッヒの補題の間の導出関係、二重否定翻訳の亜種を用いた、古典論理上の集合論ZFと直観主義論理上の集合論CZFの無矛盾性等価性についての結果が得られた。これらの成果については学術雑誌投稿論文を準備中である。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
構成的逆数学および構成的集合論の結果が当初の予想以上に得られ、これらの結果は直観主義論理上の計算可能性理論にも寄与すると考えられることから、おおむね順調に進展していると判断した。
|
| Strategy for Future Research Activity |
直観主義論理上の計算可能性理論について、次数の理論、特に優先法の研究を行う。優先法は次数構造の解析に用いる方法で、ある次数とある次数の間に、中間的な次数の存在を示す際に用いる。この際に、様々な場合分けを用いるが、この方法が直観主義論理上でも可能なものであるかを検討し、そうでなければ代替の手段の構築を試みる。目標としては、まずは再帰的集合の次数0と再帰的枚挙可能な集合の0'の間の次数の存在の直観主義論理上における証明である。
また、構成的逆数学の研究では、公理WKLと公理FANの関係についての研究を行う。特に後者はこれまで選択公理との関係が明らかになっていないことから、まずはこの観点からの特徴づけを与えた上で、WKLとの関係を解析する。
構成的集合論の研究においては、realizability interpretationと二重否定翻訳の応用による様々なモデルの構築について研究を行う。
|
| Causes of Carryover |
2020年度-2022年度の間、コロナ禍で研究が停滞したため、研究費の繰り越しがこれらの粘土で発生した。この影響で2024年度まで研究費を繰り越した。
|
