| Project/Area Number |
05J08065
|
|---|
| Research Category |
Grant-in-Aid for JSPS Fellows
|
| Allocation Type | Single-year Grants |
|---|
| Section | 国内 |
|---|
| Research Field |
Philosophy/Ethics
|
|---|
| Research Institution | Keio University |
|---|
Principal Investigator |
竹村 亮 慶應義塾大学, 文学研究科, 特別研究員(DC2)
|
|---|
| Project Period (FY) |
2005 – 2006
|
| Project Status |
Completed (Fiscal Year 2006)
|
| Budget Amount *help |
¥1,800,000 (Direct Cost: ¥1,800,000)
Fiscal Year 2006: ¥900,000 (Direct Cost: ¥900,000)
Fiscal Year 2005: ¥900,000 (Direct Cost: ¥900,000)
|
|---|
| Keywords | 論理的意味論 / 証明論 / 線形論理 / 完全性定理 / 証明の正規化定理 |
|---|
| Research Abstract |
これまでに、線形論理の最小論理と考えられるSimple Logicの中核をなす部分体系において、証明論と意味論を直接統合した証明のためのphase semanticsを導入した。その上で、証明論と論理的意味論の基本定理を統合した一元論的観点に立った基本定理を確立してきた。この部分体系は伝統的論理の最も基本的な推論を表しているが、この範囲では伝統的な論理推論の全てを表すには不十分な体系である。線形論理は、直観主義論理や古典論理等の伝統的な論理を分析するためにジラールによって導入された論理である。線形論理では、伝統的な論理において暗黙のうちに前提されていた論理構造が、様相論理結合子に関する中心的な論理推論として顕在化される。また、伝統的論理の推論はこの様相子に関する推論として、線形論理の中で完全に表現される。今年度は、BarberやPlotkinによって導入され、近年注目されているDual Intuitionistic Linear Logicと呼ばれる体系について、そこでの様相演算子の扱い方について分析した。それを基に、これまでに得られた証明のためのphase semanticsに、伝統的な直観主義論理の含意結合子を導入することで、様相演算子を部分的に導入することに成功した。(研究業績(2))
他方でゲーム意味論の分析も進めた。本研究ではまず、伝統的なLorenzen学派のゲーム意味論の分析を進め、彼らのゲーム意味論と一致する証明論的体系を取り出すことで、伝統的なゲーム意味論は証明論の枠組みで捉えることができることを示した。(研究業績(1))さらに、Laurentによって導入されたPolarized Logicに対する伝統的なLorenzen流のゲーム意味論を考え、近年計算機科学の観点から導入されているAbramsky流のゲーム意味論と対比することで二つのゲーム意味論の関係についての分析を進めた。
また、認知推論研究の観点からは、特に理論的な分析を中心に研究を進め、Ripsらのフォーマルルール理論とJohnson-Lairdらのメンタルモデルの関係の分析を行った。Johnson-Lairdの提唱するメンタルモデル理論はしばしば、図形的対象に対する図形的推論との関係が指摘されてきた。このため、証明論の自然演繹における推論規則を基にした言語的な記号操作によって推論を説明するフォーマルルール理論との対立は、言語的推論と非言語的・図形的推論との対立としても捉えられてきた。今年度は特に、このような非言語的・図形的推論の分析を進めた。(研究業績(3))
|
