有限モデル特性

数理論理学では、論理L は、 Lの任意の非定理がLの何らかの有限モデルによって偽であることが証明される場合、有限モデル特性(略して fmp)を持ちます。別の言い方をすると、Lのすべての式Aに対して、AがL定理である場合、かつAがLの有限モデル理論の定理である場合に限り、 L はfmp を持ちます。

L が有限に公理化可能で（かつ再帰的な推論規則の集合を持ち）、fmp を持つ場合、決定可能です。ただし、 Lが単に再帰的に公理化可能である場合、この結果は成り立ちません。選択できる有限モデルが有限個しかない場合でも（同型性まで）、そのようなモデルの基礎となるフレームがロジックを検証するかどうかをチェックする問題がまだあり、ロジックが有限に公理化可能でない場合は、再帰的に公理化可能であっても、決定可能ではない可能性があります。（ロジックが再帰的に列挙可能であるのは、それが再帰的に公理化可能である場合のみであり、これはクレイグの定理として知られている結果であることに注意してください。）

1つの全称量化を持つ一階述語論理式にはfmpがある。関数記号を持たず、存在量化がすべて論理式の最初に現れる一階述語論理式にもfmpがある。^[1]

• クリプキ意味論

• パトリック・ブラックバーン、マールテン・デ・ライケ、イデ・ヴェネマモーダルロジック。ケンブリッジ大学出版局、2001 年。
• アラスデア・アーカート「決定可能性と有限モデル特性」哲学論理学ジャーナル、10（1981）、367-370。