Skolem標準型:Skolem標準型是Skolem於1920年提出的一 -百科知識中文網

基本介紹

定義1Skolem標準型是如下任意一種形式的一階命題：

(∏∑型)

（1）

(∏或∑型 )

(2)(∏型)

(3)(∑型)

其中，U是不包含量詞且連線符僅僅為的公式。

第(1)種標準型顯然借鑑了亞里士多德三段論的直言命題的形式。第(1)、(3) 種標準型中的是可以消除的。消除的方法有三種。第一種是將公式中的換為，然後對於原來的約束項變為它前面的變數確定的新的變數，這樣原來的公式成為僅由全稱量詞約束的公式，原來的存在量詞約束的項的解釋縮小為由它前面的項所確定的量。如轉換為，也可寫成。如果有明確的y的解釋域，這種轉換後新的公式沒有改變與原有公式的真假值的等價性；否則真假值的等價性可能有變。第二種是將(1)公式中的換為，然後對於對U增加解釋性的關係，使得公式對於原來公式的域中不能滿足的的項增補一個非關係，進而擴大了y 的解釋域。第三種是將公式中的去掉，然後對於原來的約束項變為一個確定的解釋域中的項a，原有公式的真假值的等價性遭到破壞，但是在確定公式的無效性(永假) 時，改變後的公式與原公式具有同等意義。無論哪種方法都可以消除存在量詞。用上述同樣的方法，顯然，也可以將一階公式轉換為標準型(注意轉變後其有效性可能與原公式並不完全等價)。

總之，對於一階命題(公式)的Skolem 標準化，是基於 Skolem 標準化的定理：對於任何一階命題A，都存在一個標準型命題，使得當是可滿足的，A在其解釋域是可滿足的。

定理1 一階公式G 與G的子句集S並不相等，但是它們具有相同的不可滿足性。

證明:如果公式G 是∏型，解釋G 的域，這與子句集解釋S的域完全重合。同時，G 不能滿足，也就意味著中至少有一個子句不能滿足，此時為0；由於，此時S也為0，即Ⅱ型的不可滿足性與子句集S的不可滿足性完全相同。

如果公式G 是∏∑型或∑型，此時G將有約束的項，如果子句集中對於的解釋域設定為將與的解釋域可能不一致。但是，對於不可滿足性而言，“沒有任何一個解釋滿足G 中構成的公式”和“均不可滿足S中構成的公式”在邏輯上是一致的。可參照直言命題量詞的否定運算規則，即，它是說，“不存在”(即的不可滿足性) 意味著“”所描述的(與約束的項的)域“全都不”滿足。“”是表述在G中:而“”表述在子句集中——因為子句不再表示量詞約束意味著以項的全稱為解釋域，恰好表達了所有解釋的不滿足性。