基本介紹
- 中文名：緊緻性定理
- 外文名：Compactness theorem
- 套用學科：數學
- 適用領域範圍：符號邏輯；模型論
定義,證明,套用,
定義
緊緻性定理定義：
1）在一階邏輯中，如果我們有一個公式集合（記作）
並且 是一個不滿足式的公式集合，那么 至少有一個有限個數元素的子集（記作）
（
）並且 也是不滿足式的集合
2) 注意到，如果有一個公式集合（記作） 並且 是一個可滿足式的公式集合，那么對於所有 有限個數元素的子集（記作）
(
) ,
也是可滿足式的集合
3)也就是，前提假設我們有一個子句（Clause）集合（記作）S，並且S中的所有子句是封閉的（Clause Fermee，也就是說子句中不含有變數），如果S是不可滿足式的子句集合，若且唯若S至少有一個子集合S'，S'是有限集合併且S'是不可滿足的集合
在3)中，我們把公式集合 轉化成子句集合S，（根據定理：
）， 的可滿足性和轉化成的子句集合S的可滿足性是等價的。
證明
我們對1)的證明如下： 在證明前，我們需要知道如下定義：
a)完備性（Completude）定理的定義：前提假設我們有一個有限個數元素的子句集合（記作）S並且S中不含有變數（符號），如果S是不可滿足的集合，那么S必定擁有一個駁斥（Refutation）。
注意到當S擁有一個駁斥時，那么很顯然集合S是有限的，產生的子句
也是有限的，這是因為我們不能再運用衍生規則產生其它新的子句
c) 衍生（Derivation）的定義：從一個子句集合S,通過套用解決規則（regle de resolution）或因式分解規則（regle de factorisation）產生得到的一系列子句
叫做衍生
d) 正確性（Correction）定理的定義：前提S是一個不含變數符號的子句集合，如果子句C是子句集合S通過套用解決規則或因式分解規則所的到的子句，那么子句C是子句集合S的邏輯子序列（Consequence Logique），記作
，也就是說集合S的所有模型（或稱解釋，指派）也是子句C的模型
e) 邏輯子序列（Consequence Logique）的定義：一個公式（或公式集合）
是另一個公式（或公式集合）
的邏輯子序列，若且唯若所有
的模型（或稱解釋，指派）是
的模型，記做
證明：
根據完備性定理我們可以知道子句集合S擁有一個駁斥，那么對應的集合
也擁有駁斥，那么這兩個集合都是有限的，所以一個S的子集合S'在衍生駁斥中也是有限的，我們根據正確性定理可以知道，通過套用衍生規則,S'也是不可滿足的，那么很顯然存在對應於S'的公式集合
（
）來說，由於含有以子句形式的集合S',那么集合
必定是不可滿足的。
