2005 Fiscal Year Annual Research Report
Project/Area Number |
05J08065
|
Research Institution | Keio University |
Principal Investigator |
竹村 亮 慶應義塾大学, 文学研究科, 特別研究員(DC2)
|
Keywords | 論理的意味論 / 証明論 / 線形論理 / 完全性定理 / 証明の正規化定理 |
Research Abstract |
申請者はこれまで、線形論理の最小論理と考えられるSimple Logic (Okada 2004)の中核をなす部分体系において、完全性定理を拡張することによって強い形の正規化定理を導いた。この部分体系は伝統的論理の最も基本的な推論を表しているが、この範囲では伝統的な論理推論の全てを表すには不十分な体系である。線形論理は、直観主義論理や古典論理等の伝統的な論理を分析するためにジラールによって導入された論理である。線形論理では、伝統的な論理において暗黙のうちに前提されていた論理構造が、様相論理結合子に関する中心的な論理推論として顕在化される。また、伝統的論理の推論はこの様相子に関する推論として、線形論理の中で完全に表現される。 本研究では線形論理の中核をなす部分に様相論理結合子を導入することによって、証明のためのphase semanticsを伝統的な論理推論をも表現することのできる証明のためのphase semanticsへと拡張することを目的とし、Simple Logicの意味論であるPhase semanticsにおける様相論理結合子の分析を進めた。また、同じく線形論理の最小論理と考えられるPolarized Logicの分析も進めている。 他方で、本研究の方法論と対比するために、一元論的観点から提出されているゲーム意味論の分析を進めた。ゲーム意味論は近年、ゲーム理論的な観点からAbramskyらによって導入され注目されているが、伝統的には1950年代にLorenzen学派により対話に基づく意味論として導入された。本研究ではまず、伝統的なLorenzen学派のゲーム意味論の分析を進め、彼らのゲーム意味論と一致する証明論的体系を取り出すことで、伝統的なゲーム意味論は証明論の枠組みで捉えることができることを示した。この成果については、[R.Takemura and M.Okada 2006]にまとめられた。
|
Research Products
(2 results)