シークエント計算の新技法

2003 Fiscal Year Annual Research Report

• Project/Area Number: 14740064
• Research Institution: Tokyo Institute of Technology
• Principal Investigator: 鹿島 亮 東京工業大学, 大学院・情報理工学研究科, 助教授 (10240756)
• Keywords: 数理論理学 / シークエント計算 / 様相論理

Research Abstract

通常の様相論理の論理式でクリプキモデルの可能世界間の到達関係を表現できることはよく知られている.たとえば,論理式□A→A,□A→□□Aはそれぞれ到達関係の「反射性」,「推移性」を表しており,様相論理Kにたとえば□A→Aを公理として加えた体系の定理集合は「任意の反射的クリプキモデルで恒真な論理式の集合」に等しくなる(完全性定理).ところが到達関係の「非反射性(すなわち,どんな可能世界も自分自身へは到達できない)」を表した論理式は存在しないことも知られており,この事実は通常の様相論理式の表現能力の低さを示している.
非反射性を表現できるように様相論理式を拡張するには,可能世界の名前や到達可能性を言語に直接入れてしまう方法(hybrid logic)などいくつかが知られているが,京都大学の佐野勝彦氏が最近与えたのは,様相記号を一つ加えるだけという単純な方法でありながら記述能力が本質的に増す,というとても良い方法として注目されている.これは次のように説明できる.通常の様相論理では「到達可能なすべての世界で成り立つ」を表す様相記号□を用いるが,この他に「到達可能な自分以外のすべての世界で成り立つ」表す新しい様相記号〓を導入する.この記号を用いると,たとえば〓A→□Aが到達関係の非反射性を表すようになる.そして佐野氏は,このように言語を拡張した様相論理のいくつかの体系の完全性を,極大無矛盾集合を用いる従来の方法によって示した.
本研究では,佐野氏の完全性定理の結果を,本研究の中心的な話題である「木状のシークエント」を用いで簡潔に証明した.また現在さらに多くの拡張を試みている.

Research Products

• [Publications] Ryo Kashima: "On Semilattice Relevant Logics"Mathematical Logic Quarterly. 49・4. 401-414 (2003)
• [Publications] Katsumasa Ishii, Ryo Kashima, Kentaro Kikuchi: "Sequent Calculi for Visser's Propositional Logics"Notre Dame Journal of Formal Logic. 42・1. 1-22 (2003)