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

2017 年度 実施状況報告書

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

研究課題

研究課題/領域番号 16K16690
研究機関早稲田大学

研究代表者

秋吉 亮太  早稲田大学, 高等研究所, 准教授(任期付) (20587852)

研究期間 (年度) 2016-04-01 – 2020-03-31
キーワード論理学の哲学 / 数学の哲学 / ブラウワー / ヒルベルト / 証明論的意味論 / フッサール / ラムダ計算 / 証明論
研究実績の概要

まず,哲学的な研究の成果について述べる.第一に,高橋優太氏とのゲンツェンの無矛盾性証明についての共著論文がPhilosophical Logic: Current Trends in Asia (Springer)の第6章として出版された.(英語論文42頁)この論文では,ジーク教授が提起した「ゲンツェンの証明において内容的な要素と形式的な要素がどのように関連しているのか」という問いに一定の答えを与えた.また,ヒルベルト学派のゲンツェンの無矛盾性証明に「超限的命題に意味を与える」というブラウワー直観主義に通じる統一的で哲学的なモチーフが存在することの提案も行なった.第二に,ブラウワーのバー帰納法の議論を現代証明論のツールで再構成し,新たな解釈を与える論文を執筆した.第三に,ダメットやプラヴィッツによる直観主義的な証明論的意味論の研究をパリ第一大学のナイーボ准教授と進めた.特に,伝統的証明論のツールであったΩ規則をフランス証明論や証明論的意味論と結びつける研究に着手した.2017年9月にはパリのIHPSTで講演を行なった.第四に,フッサールの論理哲学に関して植村玄輝講師(岡山大学)とフッセリアーナ12巻,22巻の関連文献を引き続き精読した.特に,記号論や論理学と心理学に関わる論文を読み進め,共著論文に関する討論をおこなった.第五に,戦後の日本で証明論を切り開いた竹内外史の論理哲学の研究に着手し,文献調査を行った.パリ第一大学哲学科のアラナ准教授,ミュンヘン大学数学科のキュー博士と共同研究を開始した.
論理学的研究の成果としては,ミンツ教授への追悼号(国際誌 IfColog Journal)から招待され査読後に論文が出版された.関連する研究として,パラメータなしの二階ラムダ計算の「プログラムとしての複雑さ」を順序数を用いて計算した.この結果について国際会議の招待講演で報告した.

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

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

理由

今年度は哲学的研究の成果が大きかったとまとめることができる.特に,高橋優太氏と執筆した,ゲンツェンに関する論文は二年がかりで書き上げたもので,これまでの成果が出たといえるだろう.(直観主義のブラウワーと形式主義のゲンツェンにさらなる共通性が見出せたことも収穫であった.)また,ブラウワーのバー帰納法に関する論文を執筆できたことも,予期された成果が上がっているとみなせる.
ナイーボ准教授との国際共同研究については,討論の結果これからの研究の方向性がある程度定まってきた.より具体的には,Ω規則をフランス証明論の枠組みと従来の証明論的意味論を組み合わせることで説明する路線で進めている.Ω規則が想像以上に様々な文脈に適用できる可能性をもっていることも判明した.これは予期していなかった展開である.フッサールについては,最初期の関連文献の解読を継続して進めることができた.共著論文のプランも昨年度よりも具体的になってきたといえる.また,竹内外史の論理哲学の研究というテーマは予想外であったが,文献調査をある程度進めることができた.
論理学的成果については,ミンツ教授への追悼号への論文が出版されたことは計画通りであり,パラメータなしの二階ラムダ計算についての結果は予想外であった.

今後の研究の推進方策

ブラウワーのバー帰納法の議論の再検討をきっかけとして,Ω規則の哲学的文脈への応用可能性が広がってきたため,来年度はこの点を中心に探求する.(ナイーボ准教授とのパリでの共同研究を予定.)特に,当該分野において未解決問題の一つとされてきた,「数学の証明論的意味論」の構築を目指す.(これまでの証明論的意味論は,基本的に論理の範囲を専ら扱っている)より具体的には,Ω規則が適用できる範囲の数学的体系に対する証明論的意味論の構築を目標とする.ブラウワーのバー帰納法の議論については,原論文や先行研究との比較検討も行う.フッサールについてはテキストの解読が進んでいるため,来年度はドラフトの執筆開始を目標とする.必要に応じて直接会って議論する機会を設けたい.竹内外史の論理哲学の研究については,引き続きアラナ准教授やキュー博士との議論を続けて国際会議での発表と論文執筆を目指す.

パラメータなしの二階ラムダ計算についての研究については論文投稿を目指す.Ω規則の理論計算機科学への応用についても照井准教授との共同研究を進める.この方向性については今年度はあまり進展がなかったため,来年度の課題としたい.特に,代数的なアプローチも併用しつつ,高階論理のより強い部分体系への拡張を目指す.

  • 研究成果

    (7件)

すべて 2018 2017 その他

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

  • [国際共同研究] パリ第一大学/IHPST パリ科学史科学哲学研究所(フランス)

    • 国名
      フランス
    • 外国機関名
      パリ第一大学/IHPST パリ科学史科学哲学研究所
  • [国際共同研究] ミュンヘン/ルートヴィヒ・マクシミリアン大学(ドイツ)

    • 国名
      ドイツ
    • 外国機関名
      ミュンヘン/ルートヴィヒ・マクシミリアン大学
  • [雑誌論文] An Ordinal-Free Proof of the Complete Cut-Elimination Theorem for Π11-CA + BI with the ω-rule2017

    • 著者名/発表者名
      Ryota Akiyoshi
    • 雑誌名

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

      巻: 4(4) ページ: 867--884

    • 査読あり / オープンアクセス
  • [学会発表] "Proofs as Programs" Revisited2018

    • 著者名/発表者名
      Ryota Akiyoshi
    • 学会等名
      French-Japanese Workshop"Philosophy of Logic and Mathematics" with special focuses on "Philosophy of Proofs" and the Study of Euclid's Elements (Keio University)
    • 国際学会 / 招待講演
  • [学会発表] Gentle Introduction to the Omega-Rule: Part II2017

    • 著者名/発表者名
      Ryota Akiyoshi
    • 学会等名
      Atelier autour de la theorie de la dmonstration (IHPST, Paris)
    • 国際学会
  • [学会発表] A Formalization of Brouwer's Argument for Bar Induction2017

    • 著者名/発表者名
      Ryota Akiyoshi
    • 学会等名
      Workshop “Logic and Philosophy of Mathematics” (Keio University)
    • 国際学会 / 招待講演
  • [図書] Philosophical Logic: Current Trends in Asia2017

    • 著者名/発表者名
      Ryota Akiyoshi and Yuta Takahashi
    • 総ページ数
      296(6章を担当,42頁)
    • 出版者
      Springer Singapore
    • ISBN
      978-981-10-6354-1

URL: 

公開日: 2018-12-17  

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

Powered by NII kakenhi