シークエント計算の新技法
【研究分野】数学一般(含確率論・統計数学)
【研究キーワード】
シークエント計算 / 様相論理 / 厳密含意 / 完全性 / 数理論理学 / 直観主義論理 / 構成的否定
【研究成果の概要】
主に以下の二つの結果を得た.
(1)通常の様相論理では,様相記号はクリプキモデル上で二項関係(Rとする)によって真理値が定義されるが,これに「Rかつ≠」という関係で解釈される様相記号を追加する議論が最近,佐野勝彦氏(京大)を中心にして盛んになされている.
当科研費による研究では,そのようないくつかの様相論理の完全性を木状の構造を持ったシークエント計算を用いて証明した.
佐野氏はすでにカノニカルモデルによる従来の手法によって完全性を示していたが,対象となる論理に応じて従来の手法の方が簡潔にできる場合と木状シークエント計算の手法の方が簡潔にできる場合とがはっきりと分かれるという現象が明らかになった.
たとえば「推移的モデル」に対応する論理は前者,「推移的かつ反対称的モデル」に対応する論理は後者である.この違いが論理のどんな性質を反映しているのか興味深い問題であり,今後の解明が待たれる.
(2)直観主義論理のクリプキモデルの「反射的,推移的,遺伝的」という条件を変化させると,対応する論理も変わってくる.
これらは「厳密含意を持つ論理」と総称されている.
本研究ではそのような多くの論理に対して新たなシークエント計算体系を統一的に与え,完全性定理を証明した.さらに「遺伝的」の双対概念である「偽の遺伝性」に着目して,そのようなモデルを持つ論理と古典論理との関係を明らかにした.
またそれらの論理式ベースの体系化(ヒルベルト流体系)が,実質含意記号を使えば簡単であるが使わなければ困難であることを示した.
【研究代表者】
【研究種目】若手研究(B)
【研究期間】2002 - 2004
【配分額】1,500千円 (直接経費: 1,500千円)