• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 前のページに戻る

構成的逆数学の新たな展開と数学定理の計算論的意味の解明

研究課題

研究課題/領域番号 21KK0045
研究種目

国際共同研究加速基金(国際共同研究強化(B))

配分区分基金
審査区分 中区分12:解析学、応用数学およびその関連分野
研究機関東邦大学 (2023)
北陸先端科学技術大学院大学 (2021-2022)

研究代表者

石原 哉  東邦大学, 理学部, 訪問教授 (10211046)

研究分担者 河井 達治  高知大学, 教育研究部自然科学系理工学部門, 講師 (00824343)
横山 啓太  東北大学, 理学研究科, 教授 (10534430)
根元 多佳子  東北大学, 情報科学研究科, 准教授 (20546155)
藤原 誠  東京理科大学, 理学部第一部応用数学科, 助教 (20779095)
研究期間 (年度) 2021-10-07 – 2026-03-31
研究課題ステータス 交付 (2023年度)
配分額 *注記
18,980千円 (直接経費: 14,600千円、間接経費: 4,380千円)
2025年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円)
2024年度: 4,030千円 (直接経費: 3,100千円、間接経費: 930千円)
2023年度: 4,160千円 (直接経費: 3,200千円、間接経費: 960千円)
2022年度: 4,680千円 (直接経費: 3,600千円、間接経費: 1,080千円)
2021年度: 780千円 (直接経費: 600千円、間接経費: 180千円)
キーワード逆数学 / 証明論 / 構成的集合論 / 構成的算術 / 構成的位相数学 / 論理的公理の階層 / 算術的超限再帰 / 構成的逆数学 / 直観主義算術 / 論理公理の階層 / 超算術的公理 / 構成的数学 / プログラム抽出・合成
研究開始時の研究の概要

構成的逆数学の新たな展開として、算術における逆数学では直観主義算術体系において既知の公理と同値でない解析学や構成的再帰的数学の定理と同値になる新たな公理を発見する。集合論における逆数学では構成的ZF集合論において位相空間論の定理を様々な強さのNIDの同値類に分類する。
数学定理の計算論的意味の解明として、様々な公理の解析では様々な公理の性質・意味を、証明論的・モデル論的手法を用いて解析する。特に、様々な公理を解析・分離する手法を構築する。プログラム理論の構築では様々な公理に対応するプログラムの構造・性質・意味の解析を行い、公理の計算論的性質・意味を解明する。

研究実績の概要

本研究課題の算術における逆数学・集合論における逆数学・様々な公理の解析・プログラム理論の構築の研究においてそれぞれ次の実績があった。
【算術における逆数学】英国・リーズ大学の研究者と東北大学の博士課程学生とともに可述・非可述の中間領域に対応する解析学の命題の探索を継続的に行い、ドイツ・ヴュルツブルク大学の研究者とともに順序数解析と逆数学における組み合わせ命題解析の複合的手法について議論を開始した。また、弱ケーニッヒの補題(WKL)と連続性定理の関係に関する研究を行った。
【集合論における逆数学】英国・リーズ大学の研究者とともに構成的集合論における実現可能性解釈に関する研究を行った。イタリア・パドヴァ大学の研究者とともに構成的ポイントフリー位相数学におけるコーシー有限列を用いた実数の位相構造に関する研究、およびドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究者を加えサンビンが提案した基本対の概念を参考に構成的一様空間を定義しその完備化・積を与えるとともにそれらのもつ自然な性質を示した。
【様々な公理の解析】ケーニヒの補題(KL)とWKLの差を埋める公理を構成的逆数学の観点から解析し、同公理を特徴付ける関数の存在公理を特定した。また、KL とその亜種 KL!, KL!! の特徴づけに関する研究を行った。研究代表者・分担者に静岡大学の研究者を加え様々な公理の解析における最大の難所である公理間の導出不可能性を示すための有用なモデル論的手法を提案し整備した。
【プログラム理論の構築】ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究者とともにケーススタディとして擬距離に基づく構成的一様空間論の定理証明・プログラム抽出系(Minlog)への実装を行い、また基本対の概念を参考した構成的一様空間論の実装可能性について議論を開始した。

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

【算術における逆数学】計算可能性と証明論・逆数学の視点を組み合わせた研究テーマが広がりを見せ、大きなブレークスルーはないまでも着実に結果が積み上がっている。また、いくつかの関連論文の出版が完了し次なる国際共著論文の執筆にも着手しており継続的な成果発表が見込まれる。弱ケーニッヒの補題(WKL)と実関数の連続性定理に関する研究では、WKLの仮定を再帰的内包公理(RCA)に弱めることを目的としていたが従来の証明の分析に留まった。
【集合論における逆数学】構成的集合論における実現可能性解釈の応用例についての論文が出版され、さらに二重否定翻訳の応用した結果も得られた。WKLと実関数の連続性定理に関する研究では「コーシー有限列による表現が符号付きビット表現を用いた実数の位相表現と同等である」という予想を立てたが予想の厳密な証明には至っていない。構成的一様空間論は順調に構築できている。
【様々な公理の解析】構成的逆数学におけるケーニッヒの補題(KL)などの特徴づけの論文も受理され、さらに他の結果についての論文を準備中である。コロナ禍や円安の影響により海外の研究拠点をそれなりの頻度で直接訪問することが難しく未だ国際共同研究の開始には至っていない。
【プログラム理論の構築】構成的一様空間論を用いたケーススタディにとどまっており理論の構築の糸口が得られたのみである。

今後の研究の推進方策

【算術における逆数学】ラムゼイの定理の逆数学に関連する未解決問題への新たなアプローチが提唱され研究が活性化しているが、この研究テーマに順序数解析的手法を導入することで新たなブレークスルーが得られるのではないかと見込んでいる。 弱ケーニッヒの補題(WKL)と実関数の連続性定理に関する研究の目標達成には新たな観点が必要と予想されるため、問題の否定的解決の可能性も含めて従来より視野をひろげて調査・研究を行う。
【集合論における逆数学】構成的集合論における二重否定翻訳および実現可能性解釈を応用して、さらなる体系の無矛盾性・等価性の証明を試みる。予想「コーシー有限列による表現と符号付きビット表現を用いた実数の表現が同等である」に関しては、今までの研究により証明の見通しは立っているためイタリア・パドヴァ大学の研究者の協力を得て証明を試みる。今までに構築した構成的一様空間論を積分論やバナッハ空間の双対空間の解析に応用する。
【様々な公理の解析】ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究グループを直接訪問し本研究課題の研究成果について報告するとともに共同研究の構想を練る。構成的逆数学における帰納法の役割をケーニッヒの補題(KL)や計算可能性理論の観点から明らかにする。
【プログラム理論の構築】プログラム理論に関する国際研究会議に参加し関連研究についての情報収集を行い、新たな共同研究の具体的な構想を練る。ドイツ・ルートヴィッヒ・マキシミリアン大学ミュンヘンの研究グループを直接訪問し、今までのケーススタディを参考にプログラム理論に関する共同研究を立上げる。

報告書

(3件)
  • 2023 実施状況報告書
  • 2022 実施状況報告書
  • 2021 実施状況報告書
  • 研究成果

    (52件)

すべて 2024 2023 2022 その他

すべて 国際共同研究 (12件) 雑誌論文 (18件) (うち国際共著 5件、 査読あり 18件、 オープンアクセス 1件) 学会発表 (20件) (うち国際学会 15件、 招待講演 17件) 図書 (2件)

  • [国際共同研究] リーズ大学(英国)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] ルートヴィッヒ・マキシミリアン大学ミュンヘン/ヴュルツブルク大学(ドイツ)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] パドヴァ大学/ヴェローナ大学(イタリア)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] ウイーン工科大学(オーストリア)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] ワルシャワ大学(ポーランド)

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究]

    • 関連する報告書
      2023 実施状況報告書
  • [国際共同研究] リーズ大学(英国)

    • 関連する報告書
      2022 実施状況報告書
  • [国際共同研究] ルートヴィッヒ・マキシミリアン大学ミュンヘン(ドイツ)

    • 関連する報告書
      2022 実施状況報告書
  • [国際共同研究] パドヴァ大学/ヴェローナ大学(イタリア)

    • 関連する報告書
      2022 実施状況報告書
  • [国際共同研究] リーズ大学(英国)

    • 関連する報告書
      2021 実施状況報告書
  • [国際共同研究] ルートヴィッヒ・マキシミリアン大学ミュンヘン(ドイツ)

    • 関連する報告書
      2021 実施状況報告書
  • [国際共同研究] パドヴァ大学(イタリア)

    • 関連する報告書
      2021 実施状況報告書
  • [雑誌論文] Choice principles characterizing the difference between Koenig’s lemma and weak Koenig’s lemma in constructive reverse mathematics2024

    • 著者名/発表者名
      Fujiwara Makoto、Nemoto Takako
    • 雑誌名

      Computability

      巻: - ページ: 1-8

    • DOI

      10.3233/com-230478

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Ramsey's theorem for pairs, collection, and proof size2023

    • 著者名/発表者名
      Kolodziejczyk Leszek Aleksander, Wong Tin Lok, Yokoyama Keita
    • 雑誌名

      Journal of Mathematical Logic

      巻: - 号: 02

    • DOI

      10.1142/s0219061323500071

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES2023

    • 著者名/発表者名
      FUJIWARA MAKOTO、ISHIHARA HAJIME、NEMOTO TAKAKO、SUZUKI NOBU-YUKI、YOKOYAMA KEITA
    • 雑誌名

      The Bulletin of Symbolic Logic

      巻: 29 号: 3 ページ: 311-353

    • DOI

      10.1017/bsl.2023.29

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Coding of real‐valued continuous functions under WKL2023

    • 著者名/発表者名
      Kawai Tatsuji
    • 雑誌名

      Mathematical Logic Quarterly

      巻: 69 号: 3 ページ: 370-391

    • DOI

      10.1002/malq.202200031

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Choice and independence of premise rules in intuitionistic set theory2023

    • 著者名/発表者名
      Frittaion Emanuele、Nemoto Takako、Rathjen Michael
    • 雑誌名

      Annals of Pure and Applied Logic

      巻: 174 号: 9 ページ: 103314-103314

    • DOI

      10.1016/j.apal.2023.103314

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] On the decomposition of WKL!!2023

    • 著者名/発表者名
      Fujiwara Makoto、Nemoto Takako
    • 雑誌名

      Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

      巻: 381 号: 2248

    • DOI

      10.1098/rsta.2022.0010

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
    • 査読あり
  • [雑誌論文] Varieties of the Weak Koenig Lemma and the Disjunctive Dependent Choice2023

    • 著者名/発表者名
      Berger Josef、Ishihara Hajime、Nemoto Takako
    • 雑誌名

      Mathematics for Computation (M4C)

      巻: - ページ: 143-164

    • DOI

      10.1142/9789811245220_0006

    • ISBN
      9789811245213, 9789811245220
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] Bishop Metric Spaces in Formal Topology2023

    • 著者名/発表者名
      Kawai Tatsuji
    • 雑誌名

      Handbook of Constructive Mathematics

      巻: - ページ: 395-425

    • DOI

      10.1017/9781009039888.016

    • ISBN
      9781009039888, 9781316510865
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Systems for Constructive Reverse Mathematics2023

    • 著者名/発表者名
      Nemoto Takako
    • 雑誌名

      Handbook of Constructive Mathematics

      巻: - ページ: 661-699

    • DOI

      10.1017/9781009039888.025

    • ISBN
      9781009039888, 9781316510865
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Elements of Constructive Analysis2023

    • 著者名/発表者名
      Ishihara Hajime
    • 雑誌名

      Handbook of Constructive Mathematics

      巻: - ページ: 201-220

    • DOI

      10.1017/9781009039888.009

    • ISBN
      9781009039888, 9781316510865
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Constructive Functional Analysis2023

    • 著者名/発表者名
      Ishihara Hajime
    • 雑誌名

      Handbook of Constructive Mathematics

      巻: - ページ: 221-254

    • DOI

      10.1017/9781009039888.010

    • ISBN
      9781009039888, 9781316510865
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] An Introduction to Constructive Reverse Mathematics2023

    • 著者名/発表者名
      Ishihara Hajime
    • 雑誌名

      Handbook of Constructive Mathematics

      巻: - ページ: 636-660

    • DOI

      10.1017/9781009039888.024

    • ISBN
      9781009039888, 9781316510865
    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Prenex normalization and the hierarchical classification of formulas2023

    • 著者名/発表者名
      Fujiwara Makoto、Kurahashi Taishi
    • 雑誌名

      Archive for Mathematical Logic

      巻: 63 号: 3-4 ページ: 391-403

    • DOI

      10.1007/s00153-023-00899-x

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり
  • [雑誌論文] Metric fixed point theory and partial impredicativity2023

    • 著者名/発表者名
      Fernandez-Duque D., Shafer P., Towsner H., Yokoyama K.
    • 雑誌名

      Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences

      巻: 381 号: 2248

    • DOI

      10.1098/rsta.2022.0012

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり / 国際共著
  • [雑誌論文] HOW STRONG IS RAMSEY’S THEOREM IF INFINITY CAN BE WEAK?2022

    • 著者名/発表者名
      KOLODZIEJCZYK LESZEK ALEKSANDER, KOWALIK KATARZYNA W., YOKOYAMA KEITA
    • 雑誌名

      The Journal of Symbolic Logic

      巻: - 号: 2 ページ: 1-20

    • DOI

      10.1017/jsl.2022.46

    • 関連する報告書
      2023 実施状況報告書
    • 査読あり / オープンアクセス / 国際共著
  • [雑誌論文] Conservation theorems on semi-classical arithmetic2022

    • 著者名/発表者名
      Makoto Fujiwara and Taishi Kurahashi
    • 雑誌名

      The Journal of Symbolic Logic

      巻: To appear 号: 4 ページ: 1469-1496

    • DOI

      10.1017/jsl.2022.25

    • 関連する報告書
      2023 実施状況報告書 2022 実施状況報告書
    • 査読あり
  • [雑誌論文] Delta^0_1 variants of the law of excluded middle and related principles2022

    • 著者名/発表者名
      Makoto Fujiwara
    • 雑誌名

      Archive for Mathematical Logic

      巻: To appear 号: 7-8 ページ: 1113-1127

    • DOI

      10.1007/s00153-022-00827-5

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり
  • [雑誌論文] Refining the arithmetical hierarchy of classical principles2022

    • 著者名/発表者名
      Makoto Fujiwara and Taishi Kurahashi
    • 雑誌名

      Mathematical Logic Quarterly

      巻: 68 号: 3 ページ: 318-345

    • DOI

      10.1002/malq.202000077

    • 関連する報告書
      2022 実施状況報告書
    • 査読あり
  • [学会発表] Hierarchy of Σn-fragments of logical principles over HA and hierarchy of intermediate propositional logics2024

    • 著者名/発表者名
      Makoto Fujiwara,
    • 学会等名
      Dagstuhl Seminar 24021: From Proofs to Computation in Geometric Logic and Generalizations
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Reverse mathematical derivability and Weihrauch reducibility between existence statements2024

    • 著者名/発表者名
      Makoto Fujiwara
    • 学会等名
      17th International Conference on Computability, Complexity and Randomness
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Constructive uniform spaces2024

    • 著者名/発表者名
      Hajime Ishihara
    • 学会等名
      Proof, Argumentation, Computation, Modalities and Negation
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会
  • [学会発表] 構成的・可述的集合論における逆数学2024

    • 著者名/発表者名
      石原 哉
    • 学会等名
      日本数学会2024年度年会
    • 関連する報告書
      2023 実施状況報告書
    • 招待講演
  • [学会発表] Koenig's lemma, Weak Koeig's lemma and Σ-induction in constructive reverse mathematics2024

    • 著者名/発表者名
      Takako Nemoto
    • 学会等名
      Dagstuhl Seminar 24021: From Proofs to Computation in Geometric Logic and Generalizations
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Weihrauch degrees above arithmetical transfinite recursion2023

    • 著者名/発表者名
      Keita Yokoyama
    • 学会等名
      Computability and Combinatorics 2023
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Determinacy and reflection principles in second-order arithmetic2023

    • 著者名/発表者名
      Keita Yokoyama
    • 学会等名
      From omega to Omega, Workshop on Computability Theory, Set Theory and their interactions
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会
  • [学会発表] WLK implies CTM2023

    • 著者名/発表者名
      Tatsuji Kawai
    • 学会等名
      Constructive Mathematics: Foundations and Practice
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Predicative presentations of stably locally compact locales2023

    • 著者名/発表者名
      Tatsuji Kawai
    • 学会等名
      Continuity, Computability, Constructivity 2023
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会
  • [学会発表] On the decomposition of WKL!!2023

    • 著者名/発表者名
      Takako Nemoto
    • 学会等名
      Type Theory, Constructive Mathematics and Geometric Logic
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] De Morgan’s Law and Related Principles in Constructive Reverse Mathematics2023

    • 著者名/発表者名
      Takako Nemoto
    • 学会等名
      Constructive Mathematics: Foundation and Practice
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Recent results in constructive reverse mathematics2023

    • 著者名/発表者名
      Takako Nemoto
    • 学会等名
      Continuity, Computability, Constructivity 2023
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Prenex normalization and the hierarchical classification of formulas2023

    • 著者名/発表者名
      Makoto Fujiwara
    • 学会等名
      Oberwolfach Workshop ID 2346: Mathematical Logic: Proof Theory, Constructive Mathematics
    • 関連する報告書
      2023 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] 構成的数学の景色2023

    • 著者名/発表者名
      石原哉
    • 学会等名
      Logic Winter School
    • 関連する報告書
      2022 実施状況報告書
    • 招待講演
  • [学会発表] 半直観主義算術の階層と保存拡大定理2023

    • 著者名/発表者名
      藤原誠
    • 学会等名
      日本数学会 数学基礎論および歴史分科会 特別講演
    • 関連する報告書
      2022 実施状況報告書
    • 招待講演
  • [学会発表] 自然数論のモデルと逆数学2023

    • 著者名/発表者名
      横山啓太
    • 学会等名
      日本数学会 数学基礎論および歴史分科会 企画特別講演
    • 関連する報告書
      2022 実施状況報告書
    • 招待講演
  • [学会発表] Proof interpretations on finite-type arithmetic and uniform provability in reverse mathematics2022

    • 著者名/発表者名
      Makoto Fujiwara
    • 学会等名
      International Conference on Applied Proof Theory 2022
    • 関連する報告書
      2022 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] An extension of the equivalence between Brouwer’s fan theorem and weak Koenig’s Lemma with a uniqueness hypothesis2022

    • 著者名/発表者名
      Makoto Fujiwara
    • 学会等名
      Computability in Europe 2022 “Revolutions and Revelations in Computability”
    • 関連する報告書
      2022 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Spread representation of point-free real numbers2022

    • 著者名/発表者名
      Tatsumi Kawai
    • 学会等名
      Continuity, Computability, Constructivity 2022
    • 関連する報告書
      2022 実施状況報告書
    • 国際学会 / 招待講演
  • [学会発表] Real numbers from a point-free perspective2022

    • 著者名/発表者名
      河井達治
    • 学会等名
      日本数学会 数学基礎論および歴史分科会 特別講演
    • 関連する報告書
      2022 実施状況報告書
    • 招待講演
  • [図書] Handbook of Constructive Mathematics (Encyclopedia of Mathematics and its Applications)2023

    • 著者名/発表者名
      Douglas Bridges, Hajime Ishihara, Michael Rathjen, Helmut Schwichtenberg eds.
    • 総ページ数
      800
    • 出版者
      Cambridge University Press
    • ISBN
      9781316510865
    • 関連する報告書
      2023 実施状況報告書
  • [図書] 証明作法2023

    • 著者名/発表者名
      石原 哉
    • 総ページ数
      232
    • 出版者
      共立出版
    • ISBN
      9784320114890
    • 関連する報告書
      2022 実施状況報告書

URL: 

公開日: 2021-10-22   更新日: 2024-12-25  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi