様相論理のメモ。レープの定理に相当する
- L：□(□p→p)→□p
という様相論理の式（□を「証明可能」と読む）は、どういう到達可能性関係をもつフレームに対応するのか、前から気になっていた。答えは、逆整礎（converse well-founded）というフレームだそうだ。もっとも、この関係は一階の言語では記述できないようだが。
公理系KLでは
- 4：□p→□□p
が導出できる（この導出は結構難しいが、Lの図式文字pに"□p＆p" を代入すると上手くいく）。したがって、KL = KL4であり、KLのフレームの到達可能性関係は推移的でもある。
あと、どっかのサイトで、KLのフレームは非反射的（irreflexive）というのを読んだ記憶があるけど、どうもそれは有限フレームの場合の話らしい。つまり、フレームに関して
- 有限＋推移的＋非反射的
という条件を課すことと
- 有限＋推移的＋逆整礎
という条件を課すことは同値。
Postscript (2014/8/10）
KLより弱いK4にも、色々と妙な定理がある。例えば、公理系K4では、以下が証明できる。
- □◇□◇p ⇔ □◇p
