2004 Fiscal Year Annual Research Report
| Project/Area Number |
14740064
|
|---|
| Research Institution | Tokyo Institute of Technology |
|---|
Principal Investigator |
鹿島 亮 東京工業大学, 大学院・情報理工学研究科, 助教授 (10240756)
|
|---|
| Keywords | シークエント計算 / 様相論理 / 厳密含意 / 完全性 |
|---|
| Research Abstract |
主に以下の二つの結果を得た.
(1)通常の様相論理では,様相記号はクリプキモデル上で二項関係(Rとする)によって真理値が定義されるが,これに「Rかつ≠」という関係で解釈される様相記号を追加する議論が最近,佐野勝彦氏(京大)を中心にして盛んになされている.
当科研費による研究では,そのようないくつかの様相論理の完全性を木状の構造を持ったシークエント計算を用いて証明した.
佐野氏はすでにカノニカルモデルによる従来の手法によって完全性を示していたが,対象となる論理に応じて従来の手法の方が簡潔にできる場合と木状シークエント計算の手法の方が簡潔にできる場合とがはっきりと分かれるという現象が明らかになった.
たとえば「推移的モデル」に対応する論理は前者,「推移的かつ反対称的モデル」に対応する論理は後者である.この違いが論理のどんな性質を反映しているのか興味深い問題であり,今後の解明が待たれる.
(2)直観主義論理のクリプキモデルの「反射的,推移的,遺伝的」という条件を変化させると,対応する論理も変わってくる.
これらは「厳密含意を持つ論理」と総称されている.
本研究ではそのような多くの論理に対して新たなシークエント計算体系を統一的に与え,完全性定理を証明した.さらに「遺伝的」の双対概念である「偽の遺伝性」に着目して,そのようなモデルを持つ論理と古典論理との関係を明らかにした.
またそれらの論理式ベースの体系化(ヒルベルト流体系)が,実質含意記号を使えば簡単であるが使わなければ困難であることを示した.
|
