有限模型性质

有限模型性质说，无限结构不会隐藏某个只能在无限远处暴露的逻辑错误。只要公式不是定理，就能在一张有限世界图上看到失败。它把抽象的“存在反模型”变成原则上可穷举的有限证书，但证书可能很大，寻找它也可能计算昂贵。

FMP 关心的是逻辑能否由有限结构完全测试，不是所有模型本来都有限。一个公式可以同时拥有有限与无限模型；性质只要求至少有一个有限见证，不要求把每个无限模型整体等价地压成某个固定有限模型。

公式

要求观察世界拥有一个 $p$-后继和一个 $\neg p$-后继。单世界模型无法满足它：同一世界不能同时满足 $p$ 与 $\neg p$，即使加入自环也不行。两个世界已经足够：令根 $w$ 自环且满足 $p$，再令 $wRv$ 且 $v$ 不满足 $p$。这个例子给出最小有限见证的结构理由，而不是只替换一组真值。

K 的非定理 $\square p\to p$ 甚至有单世界有限反模型：取无后继世界并令 $p$ 假。方框因空后继而真，结论为假。FMP 保证这种有限反例对每个非定理都存在，但一般不会都缩到一个世界。

有限模型性质不等于有限公理化。前者限制反模型的大小类型，后者限制生成全部定理所需的公理数目；二者可以分离。FMP 也不单独推出可判定性：要把有限见证变成终止算法，还需能有效识别候选框架、枚举证明或给出可计算大小界。对 K，这些有效条件都可满足，故可判定。

它也不同于紧致性。紧致性把每个有限子理论可满足提升为整个理论可满足，可能产生无限模型；FMP 则为单个非定理或有限目标寻找有限见证。一个结论不能用另一个词直接替代。

K 的过滤上界给出一种有限搜索决策思路，并进一步成为复杂度分析的起点。实际 PSPACE 上界使用按需深度搜索等更精细技术，不会真的枚举所有 $2^{|\mathrm{Sub}(A)|}$ 状态模型；FMP 只解释有限证书为何存在。

对加入框架公理的逻辑，证明任务分成两步：保持目标公式真值，并保持框架类。例如 S4 需要传递、自反的有限过滤，不能直接拿 K 的任意商关系结束证明。某些正规模态逻辑没有 FMP，即非定理可能需要无限框架才能反驳；因此“模态逻辑通常画有限世界图”不是一般证明。

有限模型还支持自动模型生成与反例展示。工具返回的有限 Kripke 图可逐世界核对真值条款，比一份纯句法失败日志更直观；但它证明的只是当前公式在指定逻辑中不可导，不能自动概括成对所有扩展逻辑都成立的反例。