• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to previous page

Constructive reverse mathematics and its framework

Research Project

Project/Area Number 23K03205
Research Category

Grant-in-Aid for Scientific Research (C)

Allocation TypeMulti-year Fund
Section一般
Review Section Basic Section 12030:Basic mathematics-related
Research InstitutionTokyo University of Science

Principal Investigator

藤原 誠  東京理科大学, 理学部第一部応用数学科, 助教 (20779095)

Project Period (FY) 2023-04-01 – 2028-03-31
Project Status Granted (Fiscal Year 2023)
Budget Amount *help
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2027: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2025: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2024: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Fiscal Year 2023: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000)
Keywords逆数学 / 構成的数学 / 直観主義数学 / 直観主義論理 / 冠頭標準形 / 最小論理
Outline of Research at the Start

本研究は,構成的逆数学の方法論を用いて既存の数学や直観主義数学を現代的立場から再考察するものである.
本研究の中心的問いは,直観主義数学は現代数学基礎論の公理主義的立場からどのように解釈できるのか,そして直観主義数学において重要な役目を果たしていた公理は現代数学や関連する理論計算機科学とどう関連しており,どのような知見をもたらすのか,というものである.
具体的には,直観主義数学における公理や定理に対する構成的逆数学,直観主義数学を計算可能解析学や古典的逆数学と関連づけるメタ定理の開発,構成的逆数学の枠組みの見直しと整備に取り組む.

Outline of Annual Research Achievements

本研究は構成的逆数学の方法論を用いて既存の数学や直観主義数学を現代的立場から再考察するものであり,具体的な研究課題は「A. 直観主義数学における公理や定理に対する構成的逆数学」,「B. 直観主義数学を計算可能解析学や古典的逆数学と関連づけるメタ定理の開発」,「C. 構成的逆数学の枠組みの見直しと整備」に大別される.
課題Aに関し,可算関数存在公理を許容する直観主義数学や従来の構成的数学では同値となるが,弱い関数存在公理しか持たない構成的逆数学の基礎体系では同値とならない一般の決定可能ファン定理と完全二分岐木に対する決定可能ファン定理の差について詳しく解析し,根元多佳子氏(東北大学)との共同研究の成果として,その差を埋める関数存在公理を特定した.
課題Bに関しては,計算可能解析学と逆数学の直接的な関係を解析するための新たなるメタ定理の開発に取り組んでいる最中であるが,現時点で有用なメタ定理を構築するための着想が既に得られている.
課題Cに関しては,証明論的手法を構成的逆数学に応用するための基礎研究として,一階述語論理式のクラス分けについての研究を行った.特に,倉橋太志氏(神戸大学)との共同研究により,半直観主義算術における冠頭標準形定理のために2004年の先行研究において導入されていた論理式のクラスが通常の冠頭標準変換によってΣ_kやΠ_kと言われる論理式に変形されるクラスとちょうど一致していることを明らかにした.この結果は半直観主義算術における冠頭標準形定理の妥当性を保証するものである.

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

直観主義数学における公理や定理に対する構成的逆数学に関して,これまでの研究及び調査により,ケーニヒの補題や弱ケーニヒの補題に関する一部の公理の証明には原始再帰法が不可欠であることが分かってきた.ケーニヒの補題や弱ケーニヒの補題,決定可能ファン定理についてはこれまでいくつもの重要な構成的逆数学研究が行われているが,今後はそれらを原始再帰法を制限した立場から再検討し,ケーニヒの補題や弱ケーニヒの補題,決定可能ファン定理に関するより精密な構成的逆数学を展開する.
また,前年度から取り組んでいる計算可能解析学と逆数学の直接的な関係を解析するための新たなるメタ定理の開発に継続して取り組む.特に,Weihrauch還元可能性のverificationに必要な公理系の強さを測るためのメタ定理の構築を目指す.
さらに,証明論的手法を構成的逆数学に応用するための基礎研究として,直観主義論理や半直観主義論理に基づく理論においてΣ_kやΠ_kと言われる証明論的に扱いやすい形の論理式に変形される論理式の階層的クラスを構築することを目指す.

Report

(1 results)
  • 2023 Research-status Report
  • Research Products

    (6 results)

All 2024 2023

All Journal Article (3 results) (of which Peer Reviewed: 3 results) Presentation (3 results) (of which Int'l Joint Research: 3 results,  Invited: 3 results)

  • [Journal Article] Choice principles characterizing the difference between Koenig’s lemma and weak Koenig’s lemma in constructive reverse mathematics2024

    • Author(s)
      Fujiwara Makoto、Nemoto Takako
    • Journal Title

      Computability

      Volume: - Pages: 1-8

    • DOI

      10.3233/com-230478

    • Related Report
      2023 Research-status Report
    • Peer Reviewed
  • [Journal Article] EXTENDED FRAMES AND SEPARATIONS OF LOGICAL PRINCIPLES2023

    • Author(s)
      FUJIWARA MAKOTO、ISHIHARA HAJIME、NEMOTO TAKAKO、SUZUKI NOBU-YUKI、YOKOYAMA KEITA
    • Journal Title

      The Bulletin of Symbolic Logic

      Volume: 29 Issue: 3 Pages: 311-353

    • DOI

      10.1017/bsl.2023.29

    • Related Report
      2023 Research-status Report
    • Peer Reviewed
  • [Journal Article] Prenex normalization and the hierarchical classification of formulas2023

    • Author(s)
      Fujiwara Makoto、Kurahashi Taishi
    • Journal Title

      Archive for Mathematical Logic

      Volume: 63 Issue: 3-4 Pages: 391-403

    • DOI

      10.1007/s00153-023-00899-x

    • Related Report
      2023 Research-status Report
    • Peer Reviewed
  • [Presentation] Hierarchy of Σ_n-fragments of logical principles over HA and hierarchy of intermediate propositional logics2024

    • Author(s)
      Makoto Fujiwara
    • Organizer
      Dagstuhl Seminar 24021: From Proofs to Computation in Geometric Logic and Generalizations
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Reverse mathematical derivability and Weihrauch reducibility between existence statements2024

    • Author(s)
      Makoto Fujiwara
    • Organizer
      17th International Conference on Computability, Complexity and Randomness
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research / Invited
  • [Presentation] Prenex normalization and the hierarchical classification of formulas2023

    • Author(s)
      Makoto Fujiwara
    • Organizer
      Oberwolfach Workshop ID 2346: Mathematical Logic: Proof Theory, Constructive Mathematics
    • Related Report
      2023 Research-status Report
    • Int'l Joint Research / Invited

URL: 

Published: 2023-04-13   Modified: 2024-12-25  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi