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

2016 Fiscal Year Research-status Report

ブラウワー直観主義の証明論的手法による再検討

Research Project

Project/Area Number 16K16690
Research InstitutionWaseda University

Principal Investigator

秋吉 亮太  早稲田大学, 高等研究所, 助教 (20587852)

Project Period (FY) 2016-04-01 – 2020-03-31
Keywords数学・論理学の哲学 / 証明論 / 直観主義 / 形式主義 / 理論計算機科学 / ヒルベルト / ブラウワー / フッサール
Outline of Annual Research Achievements

本年度は直観主義に関する論理学的研究(数学基礎論,理論計算機科学)を中心に行い,哲学的研究も行った.
第一に,論理学的研究の成果について述べる.(i) スタンフォード大学G.ミンツ教授とΩ規則に関する共著論文が,代表的な査読付き国際誌であるArchive for Mathematical Logicから出版された.(ii) この結果を拡張した論文が,ミンツ教授への追悼号(査読付き国際誌 IfColog Journal)に招待され査読後に採択された.(iii) Ω規則を理論計算機科学へと応用する研究を,照井一成准教授(京都大学数理解析研究所)と行った.代表的な査読付き国際会議FSCDに採択され論文が出版された.(理論計算機科学分野では査読付き国際会議はジャーナルと同等かそれ以上).この結果をいくつかの国際会議で講演した.
第二に,高橋優太氏(名古屋大学学術振興会PD)とゲンツェンの無矛盾性証明について共同研究を行った.ゲンツェンの三つの無矛盾性証明を再構成し,「超限的命題に意味を与える」というブラウワー直観主義に通じる統一的なモチーフが存在することを明らかにすることで,ジーク教授の問いに一定の答えを与えた.台湾で開催された哲学的論理学の国際会議で発表し論文を投稿した.(英文37頁)
第三に,ブラウワーのバー帰納法の議論がΩ規則で再構成できるという講演を慶應大学での国際会議や,ミュンヘン大学哲学科「数理哲学センター」において講演した.これをきっかけとして,Ω規則と証明論的意味論のリンクを発見し,パリ第一大学(パンテオン・ソルボンヌ)のアルベルト・ナイーボ准教授との国際共同研究を開始した.
第四に,フッサールの論理哲学に関しては植村玄輝講師(岡山大学)とフッセリアーナ21巻,22巻の関連文献を精読し,訳やまとめを作成した.また今後の研究(論文)プランを具体的に作成した.

Current Status of Research Progress
Current Status of Research Progress

1: Research has progressed more than it was originally planned.

Reason

今年度は主に論理学的研究(数学基礎論,理論計算機科学)の成果が大きく挙がったといえる.これまでの成果を一挙に論文として出版することができたため,期待以上であった.たとえば,ミンツ教授との国際共同研究や,照井准教授との分野横断研究(数学基礎論と理論計算機科学をつなぐもの)に関する出版である.
哲学的研究については,ゲンツェンの論文(高橋優太氏との共同研究)を論文投稿までもっていくことができた.ブラウワーや証明論的意味論についても,様々な場所での講演を通じて専門家からのフィードバックを得ることができ,進展があったといえる.アルベルト・ナイーボ准教授との国際共同研究を開始できたことは予想外であった.なお,フッサールについては互いの多忙のため読んだテキストの量はそれほど多くはないが,最初期フッサールの論理哲学は未開拓な面も多く,今後の具体的な作業(たとえば論文執筆)への道筋が見えて来た.

Strategy for Future Research Activity

これまでで論理学的研究の成果は出版まで持っていくことができているため,これを継続しつつも哲学的な研究をさらに進めていきたい.Ω規則の哲学的応用は未開拓の領域であり,大きな潜在性をもっている.
哲学的応用に関する具体的な方策としては,ブラウワーに関する講演(ミュンヘンの「数理哲学センター」)は非常に好評であったため来年度には論文投稿を目指す.証明論的意味論についても,ナイーボ准教授との国際共同討議を予定している(2017年9月).
Ω規則の理論計算機科学への応用についても照井准教授との共同研究を進めていく.可能であれば,来年度中に論文を理論計算機科学の代表的国際会議に投稿したい.
フッサールについては引き続きテキスト読解を進め,これまでに見つけた『論理学研究』とのいくつかのつながりを具体的成果(発表や論文など)に結びつけることを目指す.

  • Research Products

    (11 results)

All 2017 2016 Other

All Int'l Joint Research (2 results) Journal Article (4 results) (of which Int'l Joint Research: 1 results,  Peer Reviewed: 3 results,  Open Access: 2 results,  Acknowledgement Compliant: 2 results) Presentation (5 results) (of which Int'l Joint Research: 4 results,  Invited: 3 results)

  • [Int'l Joint Research] スタンフォード大学(米国)

    • Country Name
      U.S.A.
    • Counterpart Institution
      スタンフォード大学
  • [Int'l Joint Research] パリ大学(フランス)

    • Country Name
      FRANCE
    • Counterpart Institution
      パリ大学
  • [Journal Article] An Ordinal-Free Proof of the Complete Cut-Elimination Theorem for Π11-CA + BI with the ω-rule2017

    • Author(s)
      Ryota Akiyoshi
    • Journal Title

      The Mints' memorial issue of the IfCoLog Journal of Logics and their Applications

      Volume: 4(4) Pages: 867--884

    • Peer Reviewed / Open Access
  • [Journal Article] An Extension of the Omega-Rule2016

    • Author(s)
      Ryota Akiyoshi and Grigori Mints
    • Journal Title

      Archive for Mathematical Logic

      Volume: 55 Pages: 593--603

    • DOI

      10.1007/s00153-016-0482-y

    • Peer Reviewed / Int'l Joint Research / Acknowledgement Compliant
  • [Journal Article] Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule2016

    • Author(s)
      Ryota Akiyoshi and Kazushige Terui
    • Journal Title

      1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)

      Volume: 52 Pages: 5:1--5:15

    • DOI

      10.4230/LIPIcs.FSCD.2016.5

    • Peer Reviewed / Open Access / Acknowledgement Compliant
  • [Journal Article] A uniform idea behind Gentzen’s three consistency proofs (abstract)2016

    • Author(s)
      Ryota Akiyoshi and Yuta Takahashi
    • Journal Title

      Bulletin of Symbolic Logic

      Volume: 22 Pages: 382

  • [Presentation] Brouwer's Argument of Bar Induction Revisited2017

    • Author(s)
      Ryota Akiyoshi
    • Organizer
      Colloquium in Mathematical Philosophy
    • Place of Presentation
      Munich Center for Mathematical Philosophy (Munchen, Germany)
    • Year and Date
      2017-02-23
    • Int'l Joint Research / Invited
  • [Presentation] On Brouwer’s argument of bar induction2017

    • Author(s)
      Ryota Akiyoshi
    • Organizer
      Workshop “Philosophy of logic and Mathematics - Towards Philosophy of Proofs"
    • Place of Presentation
      Keio University (Tokyo, Japan)
    • Year and Date
      2017-01-13
    • Int'l Joint Research / Invited
  • [Presentation] Opening Remarks2017

    • Author(s)
      Ryota Akiyoshi
    • Organizer
      Workshop “Philosophy of logic and Mathematics - Towards Philosophy of Proofs"
    • Place of Presentation
      Keio University (Tokyo, Japan)
    • Year and Date
      2017-01-12
    • Invited
  • [Presentation] Contentual and Formal Aspect of Gentzen's Consistency Proofs2016

    • Author(s)
      Ryota Akiyoshi and Yuta Takahashi
    • Organizer
      The joint Conference of The 3rd Asian Workshop on Philosophical Logic (AWPL-2016) & The 3rd Taiwan Philosophical Logic Colloquium (TPLC-2016)
    • Place of Presentation
      National Taiwan University (Taipei, Taiwan)
    • Year and Date
      2016-10-05
    • Int'l Joint Research
  • [Presentation] Strong normalization for the parameter-free polymorphic lambda calculus based on the Omega-rule2016

    • Author(s)
      Ryota Akiyoshi and Kazushige Terui
    • Organizer
      First International Conference on Formal Structures for Computation and Deduction (FSCD)
    • Place of Presentation
      University of Porto (Porto, Portugal)
    • Year and Date
      2016-06-22
    • Int'l Joint Research

URL: 

Published: 2018-01-16   Modified: 2022-02-16  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi