2016 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 |
本研究の目的は、20世紀前半の論理学者ゲンツェンの証明論的手法を用いて、同じく20世紀前半の数学者・哲学者ブラウワーが提示した知識論・言語論を発展させること、そして、このことから得られた洞察をもとにして数学的知識および数学言語を巡る哲学的問題にアプローチすることである。以上を踏まえ、本年度は次の4つの研究を行なった。
(a)前年度に日本科学哲学会・学会誌『科学哲学』へ投稿した論文を改訂した。本論文の主旨は、論理的含意を説明する際に生じる循環をゲンツェン的証明論を用いて回避するというものである。本成果でもって、ゲンツェン的証明論が、含意命題「AならばB」の内容の分析を与えることを明らかにした。
(b)ゲンツェン的証明論の主要成果である無矛盾性証明が、図形操作という証明論的側面だけではなく、算術命題の内容の分析という意味論的側面ももつことを検証した。この研究は、早稲田大学高等研究所准教授(任期付)・秋吉亮太氏との共同研究で進められた。この研究の成果は、研究(a)に引き続き、ゲンツェン的証明論が「命題内容の分析」においてもつ有用性を示す。
(c)ゲンツェン的証明論の発展形である「型理論」を用いて、ブラウワーの判断論を表現する論理体系である直観主義論理に相意味論(phase semantics)を与えた。この研究は、日本大学商学部准教授・竹村亮氏との共同研究で進められた。この研究成果から、証明がもつ情報を仲介としてゲンツェン的証明論とブラウワー哲学をつなぐという発想を得た。
(d)数学的証明がもつ情報をゲンツェン的証明論でもって定式化し、得られた情報概念をもとにしてブラウワー的知識論の展開を試みた。ゲンツェン的証明論とブラウワー的知識論を仲介する道具立てとして、バーワイズ・セリグマンによるチャンネル理論を用いた。現在、受入研究者である戸田山和久教授との議論を通じて研究を進めている。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
「研究実績の概要」で述べた意義をもつ成果が得られたことに加え、以下が挙げられる。まず、研究(a)において改訂した論文は、『科学哲学』への掲載が決定し出版された。次に、研究(b)の成果は、国立台湾大学で開催された第3回哲学的論理学アジアワークショップにて発表された。本成果を収録した英語論文が当ワークショップの査読付国際論文集に投稿され、現在査読中である。また、研究(c)の成果は、研究(b)が発表されたワークショップ、パリ第1大学でのワークショップそして他1件の国際学会において発表された。この成果はすでに英語論文にまとめられており、近日中に国際雑誌に投稿される予定である。
|
| Strategy for Future Research Activity |
「研究実績の概要」における研究(d)の成果を発展させ、ブラウワー的な(数学的)知識論を定式化する。そして、「ある定理の真正な理解をもつ数学者の認識状態と、公理・推論規則を巧妙に操作するパズルとしてその定理を証明できる者の認識状態とをどう区別するか」という問題に、ブラウワー的知識論を用いて取り組む。さらに、証明およびそれがもつ情報を基本概念とするブラウワー的知識論が、数学言語および数学の存在論にどのような観点を提供するかを明らかにする。
|
