A logical foundation for constructivism

• Project/Area Number: 19J01239
• Research Category: Grant-in-Aid for JSPS Fellows
• Allocation Type: Single-year Grants
• Section: 国内
• Review Section: Basic Section 12030:Basic mathematics-related
• Research Institution: Meiji University
• Principal Investigator: 藤原 誠 明治大学, 理工学部, 特別研究員(PD)
• Project Period (FY): 2019-04-25 – 2022-03-31
• Project Status: Completed (Fiscal Year 2021)
• Budget Amount: ¥4,030,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥930,000); Fiscal Year 2021: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2020: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2019: ¥1,430,000 (Direct Cost: ¥1,100,000、Indirect Cost: ¥330,000)
• Keywords: 構成的数学 / 直観主義算術 / 保存性定理 / 構成的推論 / 実現可能性解釈 / 最小論理 / ベス意味論 / BHK解釈

Outline of Research at the Start

数学や論理学の分野においてコンセンサスが乏しい構成的推論という概念に対して，現代的視座に立って数学的に妥当な定式化を与える．
ブラウアーの直観主義数学における構成的推論の形式化を目指し，1920-30年代に直観主義論理が考案された．直観主義論理はその後発展した計算機科学の理論的基盤である一方，当初の目的であった構成的推論の形式化としては弱すぎる．
本研究では，構成的推論の自然な表現である抽象実現可能性解釈という意味論に着目し，抽象実現可能性解釈が健全かつ強完全となる矛盾記号を言語に含まない形式論理で，かつ算術の公理を加えれば半直観主義有限型算術となるものを構築することを目指す．

Outline of Annual Research Achievements

本研究の目標は，BHK解釈に基づいた意味論に対して健全かつ完全となる形式論理を構築し，構成的推論を数理論理学の現代的立場から特徴付けることである. 本年度は，統語論と意味論の両側面からのアプローチを試みた．
統語論的側面からは，古典論理の証明を構成的推論と関連が深い最小論理の証明に変換する一般化されたゲンツェンの否定翻訳を詳しく解析し，それを用いて，古典算術と直観主義算術の間の保存性定理を拡張する古典算術と中間算術の間の保存性定理を得た．また，典型的な論理式のクラスに対する拡張された保存性定理と直観主義算術上の論理原理の階層構造の関係を詳しく解析し，その構造をおおよそ明らかにした．この結果は，通常の数学の証明における推論と構成的推論の差を詳しく解析するために有用であると思われる．これらは倉橋太志氏(神戸大学)との共同研究の成果である．さらに，BHK解釈に基づく意味論に対して健全かつ完全となる形式論理の構築のための足がかりとなる選言記号及び矛盾記号を含まない有限型算術及びその自然な拡張の詳しい解析を進め，問題の適当な定式化のための着想を得た．
意味論的側面からは，中間命題論理を分離するクリプキモデルを用いて中間算術の階層を分離する一般的な手法を精査して改良した．また，最小論理に対して健全かつ完全であることが構成的に示される意味論であるSchwichtenberg氏の木意味論について，直観主義論理で証明可能であることの特徴付けに関する新たなる知見を得た．さらに，木意味論とクリプキ意味論の関係について調査と分析を行い，その関連性を数学的に記述するための端緒を得た．

Research Progress Status

令和3年度が最終年度であるため、記入しない。

Strategy for Future Research Activity

令和3年度が最終年度であるため、記入しない。

Research Products

• [Journal Article] Delta^0_1 variants of the law of excluded middle and related principles (2022)
  • Author(s): Makoto Fujiwara
  • Journal Title: Archive for Mathematical Logic Volume: To appear Issue: 7-8 Pages: 1113-1127
  • DOI: 10.1007/s00153-022-00827-5
  • Peer Reviewed
• [Journal Article] Conservation theorems on semi-classical arithmetic (2022)
  • Author(s): Makoto Fujiwara and Taishi Kurahashi
  • Journal Title: The Journal of Symbolic Logic Volume: To appear Issue: 4 Pages: 1469-1496
  • DOI: 10.1017/jsl.2022.25
  • Peer Reviewed
• [Journal Article] Decidable fan theorem and uniform continuity theorem with continuous moduli (2021)
  • Author(s): Makoto Fujiwara and Tatsuji Kawai
  • Journal Title: Mathematical Logic Quarterly Volume: 67 Issue: 1 Pages: 116-130
  • DOI: 10.1002/malq.202000028
  • Peer Reviewed
• [Journal Article] Koenig's lemma, weak Koenig's lemma, and the decidable fan theorem (2021)
  • Author(s): Makoto Fujiwara
  • Journal Title: Mathematical Logic Quarterly Volume: 67 Issue: 2 Pages: 241-257
  • DOI: 10.1002/malq.202000020
  • Peer Reviewed
• [Journal Article] Prenex normal form theorems in semi-classical arithmetic (2021)
  • Author(s): Makoto Fujiwara and Taishi Kurahashi
  • Journal Title: The Journal of Symbolic Logic Volume: 86 Issue: 3 Pages: 1124-1153
  • DOI: 10.1017/jsl.2021.47
  • Peer Reviewed
• [Journal Article] Characterising Brouwer's continuity by bar recursion on moduli of continuity (2020)
  • Author(s): Makoto Fujiwara and Tatsuji Kawai
  • Journal Title: Archive for Mathematical Logic Volume: 60 Issue: 1-2 Pages: 241-263
  • DOI: 10.1007/s00153-020-00740-9
  • Peer Reviewed
• [Journal Article] A Logical Characterization of the Continuous Bar Induction (2020)
  • Author(s): Makoto Fujiwara and Tatsuji Kawai
  • Journal Title: Book: F. Liu, H. Ono, and J. Yu, editors, Knowledge, Proof and Dynamics: The Fourth Asian Workshop on Philosophical Logic Volume: - Pages: 25-33
  • DOI: 10.1007/978-981-15-2221-5_2
  • ISBN: 9789811522208, 9789811522215
  • Peer Reviewed
• [Journal Article] Bar Induction and Restricted Classical Logic (2019)
  • Author(s): Makoto Fujiwara
  • Journal Title: Logic, Language, Information, and Computation, Lecture Notes in Computer Science Volume: 11541 Pages: 236-247
  • DOI: 10.1007/978-3-662-59533-6_15
  • ISBN: 9783662595329, 9783662595336
  • Peer Reviewed
• [Journal Article] Equivalence of bar induction and bar recursion for continuous functions with continuous moduli (2019)
  • Author(s): Makoto Fujiwara and Tatsuji Kawai
  • Journal Title: Annals of Pure and Applied Logic Volume: 印刷中 Issue: 8 Pages: 867-890
  • DOI: 10.1016/j.apal.2019.04.001
  • Peer Reviewed
• [Presentation] Conservation theorems on semi-classical arithmetic (2021)
  • Author(s): Makoto Fujiwara
  • Organizer: New Frontiers in Proofs and Computation
  • Int'l Joint Research / Invited
• [Presentation] Conservation theorems on semi-classical arithmetic (2021)
  • Author(s): Makoto Fujiwara
  • Organizer: Dagstuhl Seminar 21472: Geometric Logic, Constructivisation, and Automated Theorem Proving
  • Int'l Joint Research / Invited
• [Presentation] Bar induction and restricted classical logic (2019)
  • Author(s): Makoto Fujiwara
  • Organizer: 26th Workshop on Logic, Language, Information and Computation
  • Int'l Joint Research
• [Presentation] ゲーデルによる算術の無矛盾性証明と構成主義 (2019)
  • Author(s): 藤原誠
  • Organizer: 科学基礎論学会秋の研究例会