様相論理

Correspondenceと名前の由来

• D(φ) := □φ→◇φ
  • seriality
  • 義務論理に使われるので、義務的を意味するDeonticあたりからっぽい
• T(φ) := □φ→φ
  • reflexivity
  • Gödel の system T かららしい (参考: <URL:http://home.utah.edu/~nahaj/logic/structures/axioms/CLpp.html>)
• B(φ) := φ→□◇φ
  • symmetry
  • Brouwerかららしい。
• 4(φ) := □φ→□□φ
  • transitivity
  • C.I.LewisのS4から
• 5(φ) := ◇φ → □◇φ
  • euclidean (aからb,cに到達可能なら、bからcに到達可能(もちろんcからbにも到達可能))
  • C.I.LewisのS5から
• P(φ) := φ→□φ
  • pathetic
• Q(φ) := ◇φ→□φ
  • deterministic
• R(φ) := □□φ→□φ
  • dense
• G(φ) := ◇□φ→□◇φ
• L(φ) := □T(φ)→□φ
  • transitive and well-founded
• M(φ) := □◇φ→◇□φ

ツール

• AiML: Tools にツールが結構まとまっている

その他

• ヒビルテ [modal-logic]