| 研究課題/領域番号 |
17H02265
|
|---|
| 研究機関 | 慶應義塾大学 |
|---|
研究代表者 |
岡田 光弘 慶應義塾大学, 文学部(三田), 教授 (30224025)
|
|---|
| 研究分担者 |
秋吉 亮太 早稲田大学, 高等研究所, その他(招聘研究員) (20587852)
金子 洋之 専修大学, 文学部, 教授 (60191988)
峯島 宏次 お茶の水女子大学, 文理融合 AI・データサイエンスセンター, 特任准教授 (80725739)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2022-03-31
|
| キーワード | 証明 / 論証 / 論理の哲学 / 数学の哲学 / ウィトゲンシュタイン / 証明の哲学 / 証明論的・型論的意味論 / 図的表現と図的推論・判断 |
|---|
| 研究実績の概要 |
「規則に従う」についてのWittgensteinの議論がWittgenstein自身の中でどのように変化していったかを検討した。Wittgensteinがこのテーマを取り扱った初期の時点でWaismannに与えた影響に注目した。Waismannのバージョンを整理すると同時に、「青表紙本」などとの関係についても考察した。これまでの我々の「規則に従う」に関する一連の研究に新たな視点を与えた。
セキュリティ、プライバシー、公正性などの論理的定義と暗号プロトコルの述語論理的セキュリティ検証理論を発展させた。特にCoq証明支援系によるセキュリティやプライバシーに関する種々の性質や概念を論理的に捉えて、その性質を証明す仕方を検討した。これまではForcingモデル構成法の一種を用いていたが、nondistinguishability概念をベースにした手法も検討した。
序構造による計算の強正規化証明は、一方で証明論において、他方で項書き換え理論においてほぼ独立に研究されてきた。証明（またはそのカリー＝ハワード対応の意味での型付きラムダ項）の強正規化に焦点を当てる証明論とより自由な代数的計算体系についての項書き換え理論とを結びつける試みの一つとして、Howardによるラムダ抽象・適用の解釈を項書き換え論的視点から意味論的道具立ての若干の消去を試みた。
図形推論及び図的表現を用いた判断・意思決定の研究を通じて、推論・論証の図的側面を検討した。論証の図的分析の典型としてのTakeuti Ordinal Diagramsを哲学的・論理学的に分析した。
日常言語のタイプ論的意味論による分析を進展させた。論理の必然性についての考察も進んだ。以上、全ての成果を出版・公表した。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
1: 当初の計画以上に進展している
理由
証明・論証の哲学についての研究計画の主要な各事項が予想以上に進展した。証明の図的理解や一般化された定基順序構造との関係を証明論と計算論の観点から考察した。これをヒルベルト学派の証明の図的理解や証明正規化の有限主義的分析の観点から考察した。例えば、中期Wittgenstein哲学における論証と計算の哲学を前年度に続いて明らかにするとともに、前期と後期の「規則」についての検討に発展させた。Waismannとの関係や、inductive typeのwittgensteinの表現を解明し、それが初期のラッセル型理論批判とどう整合するかを検討した。形式言語と証明の関係を再検討した。形式的言語が先に前提された形式論理の考え方から、基礎概念の形式的特徴付けが形式言語に先行する立場への移行について、我々の見方をいくつかの具体的ケーススタディで考察し始めた。例えば、ネットワーク社会の通信や情報共有の安全性や公平性の証明付き保証に、このような新しい形式化の考えを適応する検討を進めた。
日常言語による推論のこれまでの被験者実験の成果を整理した。特に論理的推論能力と合理的意思決定・判断とに関わる成果を整理し、論証・合理的意思決定・判断における図的効果についてさらなる実験デザインを「論証」の哲学」の視点から考察した。
|
| 今後の研究の推進方策 |
これまでの本課題研究の研究成果を整理するとともに、これらを基にさらに論証・証明についての哲学研究を発展させていく。形式的推論と日常の言語による推論の比較、形式的証明と日常の論証の比較、図的推論による論証と言語的論証の比較、論証・証明と計算の関係などを、これまでの間我々が導入してきた研究手法でさらに解明していく。論証と計算の比較に関しては、様々のquasi-well orderings理を仲介する手法により検討していく。図的推論と言語的推論の比較に関しては、意思決定課題研究との関連も含めて検討していく。ヒルベルト学派の証明論、ウィトゲンシュタインの証明論、フッサールの証明論、日本が生んだ世界的数理論理学者であった竹内外史の証明論の哲学的側面、直観主義学派の証明構成論など広範囲な証明に関する理論を我々の「証明の哲学」の下で捉え直す。哲学手法を基本としながら、数理的手法、情報科学・認知科学的手法、心理学実験手法なども取り入れた総合的研究手法を本年度も用いていく。本研究の形式証明についての研究を通じて、概念の形式的特徴づけについての応用研究も試みる。特にケーススタディの一つとして、ネットワークコミュニケーション環境におけるsecurityなどの特徴付けとその形式証明などこれまで本グループが行ってきたが、その成果をalgorithmic ethicsの公平性、説明性などの基礎概念の特徴付けとその証明の問題へ応用することを試みる。また、我々の「証明の哲学」の成果を自然言語の論証の分析に応用する。
|
