跳慮跋考

興味も思考も行先不明

様相論理の可能世界意味論のイメージ

調べた内容の私的な解釈を書いた感じなので用心されたい。

命題について、述語論理が「どんな対象について成り立つか」を扱う様に、様相論理は「どの程度成り立つか」を扱う。様相論理は世界(解釈とその上で成り立つ論理式の集まり)自体を記述し、命題に対する評価を考える。

論理式αに対して

  • □α ≡ ¬◇¬α
  • ◇α ≡ ¬□¬α

を定義し、□(box)と◇(diamond)を様相演算子と呼ぶ。
□αは「αは必然的である」、◇αは「αは可能である」という概念を形式化したものと捉えられる。実際 ¬□¬α ⇔ ◇α は「αでない事は必然ではない」=「必ずαでない訳ではない」=「αは可能である」と考える事ができる。
必然的を「全ての世界で成り立つ」、可能を「成り立つ世界がある」と捉えれば世界に対する量化とも言える。しかし、□α や ◇α という論理式自体も一つの世界に立つ存在なので、「全ての世界で成り立つ」という様に俯瞰的に世界達へ言及する事はできないのである。
そこで、「全ての世界」を「自分の世界から見える(到達可能な)世界全て」と修正する。到達可能性の範囲によって色々な公理系が考えられる。
(飽く迄公理系というのは意味論とは独立に、構文論上で定義できるが、概念を把握するには「到達可能な世界がどう規定されるか」という意味論的なところを同時に考えた方が分かり易いと思い以下の様に構成した。こうした(到達)可能世界意味論は様相論理の意味論の一つでしかないという事は十分に強調されなくてはならない。)

K (Kripkeによる体系)

命題論理に

  • 必然化規則「αが定理である時、□αも定理である」
  • 分配公理 □(φ→ψ)→(□φ→□ψ)

という規則・公理を加えた体系。
定理とは「妥当な論理式」=「全ての解釈で真な論理式」であり、αが定理かどうかは論理体系にのみ依存するので、必然化規則は「全ての世界」で論理体系は同一である事の帰結である。
到達可能世界は全ての世界の部分集合であるから、到達可能性が以下の公理でどう拡張されようともこれは成り立つだろう。
必然化規則は決して α→□α ではない。この論理式が表すのは「この世界でαが真ならば全到達可能世界でも真」という乱暴な一般化である。
分配公理は「□(φ→ψ)∧□φ ならば □ψ」という世界全体についての modus ponens と考えられ、到達可能世界の範囲がそれぞれの論理式で同一である事を表す。

T (Gödelによる)

Kに次の公理を加える。

  • □α→α

これは到達可能な世界に自分自身を含める。
到達可能の関係を⇝で表せば、これは W⇝W (反射律)が常に成り立つ事を言う。
{ W₁, W₂, W₃ }という3つの世界があるとすれば、
f:id:quinoh:20130428134744p:plain
という到達可能性が最低限存在するという事である。
この様な世界の集合、その間の到達可能性、そして各世界で成り立つ命題を合わせたものをKripke構造と呼ぶ。

B (Brouwerによる)

Tに次の公理を加える。

  • α→□◇α

これは全到達可能世界から自分が到達可能である事を表す。
W₁⇝W₂ ならば W₂⇝W₁ (対称律)を言う。
f:id:quinoh:20130428134758p:plain(*)
という到達可能性があれば、実は
f:id:quinoh:20130428135131p:plain
となっているという事である。

S4 (Lewisによる)

Tに次の公理を加える。

  • □α→□□α

これは「到達可能な世界から到達可能な世界」が到達可能である事を示す。
W₁⇝W₂ かつ W₂⇝W₃ ならば W₁⇝W₃ (推移律)を言う。
(*)の図の場合に
f:id:quinoh:20130428135453p:plain
となっているという事である。

S5 (Lewisによる)

S4に次の公理を加える。

  • ◇α→□◇α

これは「自分の到達可能な世界」が「自分の到達可能世界からの到達可能な世界」と同じである事を示す。
W₁⇝W₂ かつ W₁⇝W₃ ならば W₂⇝W₃ を言う。
S4の図について実際は
f:id:quinoh:20130428140542p:plain
となっているという事である。

平尾始氏及び上村芳郎氏の頁を参考にした。
また図はCarl Burch氏のAutomaton Simulatorによる出力を加工し用いた。