様相論理のメモ。文献を見ていると、S4.3を特徴づける公理型は
- ◇P＆◇Q → ◇(◇P＆Q)∨◇(◇Q＆P)
- □(□P→Q)∨□(□Q→P)
の2種類あるようだ*1。これらが同値であることは体系Kで証明できる。これらに対応するフレーム<W, R>の到達可能性関係は、以下。
- wRu ＆ wRv → uRv v vRu
面倒なのは、これらとは少し違う定式化もあるらしいことだ。
- ◇P＆◇Q → ◇(◇P＆Q)∨◇(◇Q＆P) v (P＆Q)
- □(P＆□P→Q)∨□(Q＆□Q→P)
これらに対応するフレーム<W, R>の到達可能性関係は以下。
- wRu ＆ wRv → uRv v vRu v u=v
こちらの定式化は、さっきの定式化と同値にならない。ただし、到達可能性関係が反射的ならば、違いはつぶれてしまう（任意のuについてuRuだから、u=vのときにはuRvとなるから・・・）。
Postscript (2014/8/13)
更に別の公理型として
- □(□P→□Q)∨□(□Q→□P)
を立てるやり方もある。対応するフレーム<W, R>の到達可能性関係はたぶん
- wRu ＆ wRv → [(uRx → vRx) v (vRx → uRx)]
なのではないかな・・・。この関係と、
- wRu ＆ wRv → uRv v vRu
は独立である。前者から後者を導出するには反射性を、後者から前者を導出するには推移性を仮定する必要がある。
関連記事
*1:時間論理ではこの公理をよく見かける。Ａ. プライアーがS4では時間論理としては弱すぎると考えたことに由来するようだが…。
