有限モデル性
>次の2条件は同じことを主張しており、この性質をLの有限モデル性(finite model property)と呼ぶ
>(A) 任意のL論理式\varphiに対して次が成り立つ. \varphiがL充足可能ならば, \varphiはある有限Lモデルで充足される
>(B)任意のL論理式\varphiに対して次が成り立つ. \varphiがL恒真でないならば, ある有限Lモデルとその中のある状態で\varphiが偽になる
ここでのLとは以下のいずれかのこと
K
CTL
様相ミュー計算
PDL
このいずれの体系でも上記の性質が成り立つ
Small Scope Hypothesisと関連ありそうだけどどうだろう