2017 Fiscal Year Annual Research Report
ゲンツェンの証明論的手法を用いたブラウワーの知識論および言語論の再構築
| Project/Area Number |
16J04925
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
高橋 優太 名古屋大学, 情報学研究科, 特別研究員(PD)
|
|---|
| Project Period (FY) |
2016-04-22 – 2019-03-31
|
| Keywords | 論理学の哲学 / 数学の哲学 / 数学基礎論 / 数理論理学 / 証明論的意味論 / 情報の哲学 |
|---|
| Outline of Annual Research Achievements |
本研究課題は、現代論理学の一分野であるゲンツェン的証明論を用いて、ブラウワーによる知識論・言語論を発展させ、知識および言語を巡る数理哲学上の問題にアプローチするというものである。二年目となる本年度は以下の研究(1),(2a),(2b),(3)を行なった。
(1)ゲンツェン的証明論のより深い理解のための研究：竹内外史が、ゲンツェン的証明論を拡張する過程で導入した「順序図形(ordinal diagrams)」について、特にその整列性に関して数学的研究を行なった。本研究は慶應義塾大学文学部教授・岡田光弘氏との共同研究で進められた。
(2)ゲンツェン的証明論とブラウワーの知識論・言語論とを結びつけるための研究：
(2a)ゲンツェンによる算術の無矛盾性証明は、算術命題の意味を、完結した無限(実無限)の概念に依拠せずに説明することを目指すものであったことを歴史的手法および数学的手法両方を用いて検証した。本研究は、部分的に、早稲田大学高等研究所准教授(任期付)・秋吉亮太氏との共同研究で進められた。
(2b)二階直観主義命題論理の含意・全称量化子断片と、一階最小命題論理とに対して、ゲンツェン的証明論に基づく意味論である「証明論的意味論」を与えた。本研究は日本大学商学部准教授・竹村亮氏との共同研究で進められた。
(3)ゲンツェン的証明論によるブラウワーの知識論・言語論の展開：研究(1),(2a),(2b)を踏まえ、数学的証明がもつ情報をゲンツェン的証明論でもって定式化し、このようにして得られた情報概念をもとにブラウワー的知識モデル・言語モデルを構築することを目指した。受入研究者である戸田山和久教授との議論を踏まえ、本年度では、数学的証明がもつ情報を捉えるための理論としてゲンツェン的証明論だけでなくドレツキの情報意味論も用いた。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
おおむね順調に進展していると自己評価した理由としては、以下のようにして定期的な成果報告ができたことが挙げられる。
研究(1)については、その成果の中間報告として、慶應義塾大学にて開催された「数学・論理学の哲学」日仏ワークショップにて岡田光弘氏と共同発表をした。
研究(2a)は二つの論文にまとめられた。一つ目は、秋吉氏との共著で執筆され、第三回哲学的論理学アジアワークショップの査読付国際論文集に掲載が決定し出版された。二つ目は、科学基礎論学会発行の査読付欧文誌に掲載が決定した。また、二つ目の論文の内容は、草津セミナーハウスにて開催された数理哲学史夏期合宿セミナーにおいて発表された。
研究(2b)における二階直観主義命題論理の含意・全称量化子断片に対する成果は、竹村氏との共著により論文にまとめられた。その論文は国際学術雑誌に投稿され、現在査読中である。一階最小命題論理に対する成果は、ストックホルム大学において開催されたLogic Colloquium 2017において発表された。
研究(3)では次のトピックに関する中間報告を行なった：数学の定理の真正な理解をもつエージェントの認識状態と、公理と推論規則を巧妙に操作するパズルとしてその定理を証明できるエージェントの認識状態を区別できるような、ブラウワー的知識モデル・言語モデルを構築することを目指した。中間報告は、アルカディア市ヶ谷にて開催された日本論理哲学会第21回大会においてなされた。
|
| Strategy for Future Research Activity |
本研究課題の最終年度の推進方策は以下である。戸田山教授との議論、および、日本論理哲学会大会での議論によって、課題達成のためには数学的証明自体というよりは証明を生み出す行為(action)に着目すべき、という発想が得られた。申請者は、エージェントの認識状態を巡る上記の哲学的問題へとアプローチするにあたって、この発想が手がかりになると現在考えている。この発想は、エージェントの認識状態に対してきめの細かい分析を与えるブラウワー的知識モデル・言語モデルをもたらしうる。最終年度における課題は、この発想を具体化するゲンツェン的理論を整備すること、そして、そこで得られた理論を用いてブラウワー的知識モデル・言語モデルを構築し、エージェントの認識状態を巡る問題へアプローチすることである。引き続き戸田山教授との議論を通じて、本課題の達成を目指す。
|
