05_第三部分1

（1） 若A由前面的两个公式B及BA用MP得到，则由󰀀B，及󰀀BA及归

纳假设知由B与BA的证明长度已少于n，均逻辑有效。由逻辑有效的MP知A逻辑有效。 （2） 若A由前面某项B用Gen得到，即A=(xi)B，则由󰀀B及归纳假设，B逻

辑有效，由逻辑有效的等价描述知(xi)B逻辑有效。至此，证明了可靠性定理。

1、 K的相容性：

命题：K是相容的，即AF,A与A不能都是定理。

证明：这是可靠性定理的直接推论，因为A与A不能同时为逻辑有效的公式。

（四）演绎定理

为了给完备性作准备，我们还要对形式系统K的演绎作一些讨论。于在K中有量词和Gen规则，所以K中的演绎要比L中演绎复杂得多。例如，显然A(xi)A不是逻辑有效的，从而由K的可靠性定理知A(xi)A不是定理，即󰀀A(xi)A不成立，但是

A󰀀(xi)A，这因为：

（1）A 假设， （2）(xi)A Gen。

由此可知，L中的演绎定理“若Γ{A}󰀀B，则Γ󰀀AB”在这里成立了。原因就在于Gen中没有对变元作任何要求。解决这一问题的办法有两种，要么不用Gen，要么用Gen时对变元作要求。 1、演绎定理及其推论

（1） 演绎定理：设ΓF，A，BF，若Γ{A}󰀀B，且对每个在A中自由出现

的变元x，在从Γ{A}到B的推演中没有使用过Gen（关于x的），则

Γ󰀀AB。

证明：我们用归纳法证明,关于从Γ{A}到B的推演长度n作归纳。n=1，显然可用L中方法证明。设n>1，且对从Γ{A}到C的推演长度小于n时，在定理条件下Γ󰀀AC。现对n，若B为公理或为A或为Γ中公式，则由归纳假设已得证明。若B由前面两项用MP得到，则也可象L中的证明一样证明。现在就剩下一种情况

B=(xi)C，这里C为从Γ{A}到B的推演中的一项，这样从C到

(xi)C=B就用到了Gen，由定理条件知xi不在A中自由出现。由归纳假设，存在

从Γ到AC的推演。

65

(1)

.

. 从Γ到AC的推演 .

(k) AC

这个推演可以补充成Γ到AB的推演

(k+1) (xi)(AC) (k)Gen

(k+2) (xi)(AC)(A(xi)C) (K6) (k+3) A(xi)C=B (k+1)(k+2) ,MP 所以Γ󰀀(AB)

（2） 闭公式的演绎定理：设Γ{A}󰀀B，A为闭公式，则Γ󰀀AB。 （3） 三段论规则(HS规则)，{AB,BC}󰀀AC。

证明：因为{AB,BC}{A}󰀀C

其实①A 假设 ②AB Γ

③B ①②MP ④BC Γ

⑤C ③④MP

这其中并没有用到Gen，故由演绎定理有{AB,BC}󰀀AC

（4） 演绎定理的逆定理，若Γ󰀀AB，则Γ{A}󰀀B。 证明：①Γ󰀀AB

②A 假设 ③B ①②MP

2、例

（1） 证明设xi不在A中自由出现，则

󰀀(A(xi)B)(xi)(AB)

(这是(K6)的逆定理)

证明：①A(xi)B 假设 ②(xi)BB (K4)

③AB ①②HS ④(xi)(AB) ③Gen

66

这里xi不在A 中自由出现，所以也不在A(xi)B中自由出现，所以在上述证

明A(xi)B󰀀(xi)(AB) 中关于xi用了Gen，但xi不自由出现，所以可由演绎定理知󰀀(A(xi)B)(xi)(AB)。 （2） 证明：（i）(xi)(AB)󰀀(xi)┐B(xi)┐A

（ii）󰀀(xi)(AB)((xi)A(xi)B)

证明：（i）先证{(xi)(AB), (xi)┐B}󰀀(xi)┐A

①(xi)(AB) 假设 ②(xi)┐B 假设 ③(xi)(AB)(AB) (K4) ④AB ①③MP ⑤(AB)(┐B┐A) 重言式 ⑥┐B┐A ④⑤MP ⑦(xi)┐B┐B (K4) ⑧┐B ②⑦MP

⑨┐A ⑥⑧MP ⑩(xi)┐A ⑨Gen

在上述证明中只用过一次关于xi的Gen,且xi在(xi)┐B中不自由出现，所以由上述证明和演绎定理知有

(xi)(AB)󰀀((xi)┐B(xi)┐A)

（ii）由于L中的重言式的代换实例为K中定理，所以(P1 P2)(┐P2 ┐

P1)的一个代换实例((xi)┐B(xi)┐A)(┐(xi)┐A┐

(xi)┐B)

为K中定理，由此式和（i）用MP可得到

(xi)(AB) 󰀀(┐(xi)┐A┐(xi)┐B)

=(xi)A(xi)B

67

而在这一推演没有对(xi)(AB)中自由出现的变元用过Gen，自然可用演绎定理，从而有󰀀(xi)(AB) ((xi)A(xi)B)。

二、可证等价与代换定理

为了证明完备性，我们也和命题逻辑中一样先建立可证等价关系以及谓词逻辑中的代换定理。

（一）可证等价关系

1、可证等价的概念

（1） 定义：设A、BF，若AB与BA都是K中的定理，则称A与B可证等价，记作A～B （2） 可证等价的刻划 命题：设A、BF，则A～BAB=(AB)(BA)为定理 证明：因为(AB)(BA)=┐((AB)┐(BA)) 由L中的重言式CDC，CDD知

󰀀┐(C┐D)C, 󰀀┐(C┐D)D,

由MP知当┐(C┐D)为K中定理时，C，D均为K中定理，所以当AB为K中定理时AB与BA都是定理，故A～B。 反过来，设AB与BA为定理，则因为

󰀀C(D┐(C┐D)) 即 󰀀C(DCD)

所以，由󰀀AB，󰀀BA知󰀀AB。

（二）可证等价的性质

1、可证等价的逻辑等价性（可靠性）

命题：设A，BF，若A～B，则AB，即可证等价的公式也是逻辑等价的。 证明：这也是可靠性定理的推论。 2、可证等价是公式集F上的等价关系

命题：（1）A～A （反身性）

（2）A～B则B～A （对称性）

68

（3）A～B，且B～C，则A～C （传递性）

证明：（1）（2）由定义可知，（3）由定义用HS可证。 3、 可证等价对运算的保持性

命题： （1）若A～B，则┐A～┐B；

（2）若A～B，C～D，则AC～BD；

（3）若A～B，C～D，则AC～BD，AC～BD； （4）若A～B，则(xi)A～(xi)B，(xi)A～(xi)B。

󰀀┐B ┐A，证明：(1)设A～B，则󰀀A,又󰀀(AB)(┐B┐A),由MP，

同理󰀀┐A┐B，故┐A～┐B

(2)A～B，C～D，因为󰀀CD和󰀀(CD)(A(CD)), 由MP󰀀A(CD)，再由(K2)󰀀(A(CD))

((AC)(AD))。所以󰀀(AC)(AD)。

同理可证󰀀(AD)(AC)，这样得到(AC)～(AD)。 类似可证：AD～BD，所以有AC～BD。

(3)由(1)(2)可得。

(4)设A～B，则󰀀AB，由(K4)󰀀(xi)AA。所以由HS得

󰀀(xi)AB，即(xi)A󰀀B（演绎定理的逆定理）。由Gen得

(xi)A󰀀(xi)B，但xi不在(xi)A中自由出现，所以由演绎定理，得

󰀀(xi)A(xi)B，同理可证得󰀀(xi)B(xi)A。从而知

(xi)A～(xi)B。因为xi=┐(xi)┐,

故由上述证明可得(xi)A～(xi)B。

（三）代换定理

69

有了可证等价性，就可得到如下的代换定理。 1、变元代换定理

命题：设A(xi)F，xi为A(xi)中的自由变元，且A(xi)中不含变元xj，则

(xi)A(xi)～(xj)A(xj)

（这里A(xj)就是把A中出现的xi代换成xj得到的公式） 证明：先证明󰀀(xi)A(xi)(xj)A(xj)。

为此要证(xi)A(xi)󰀀(xj)A(xj)，

①(xi)A(xi) 假设

②(xi)A(xi) A(xj) (K5)（这里t= xj 关于A(xi)中xi是自由的） ③ A(xj) ①②MP ④(xj)A(xj) ③Gen 所以(xi)A(xi)

󰀀(xj)A(xj)

在上述推演中用了(xj)的Gen，但xj不在(xi)A(xi)中自由出现，所以由演绎定理󰀀(xi)A(xi)(xj)A(xj)。

再证󰀀(xj)A(xj)(xi)A(xi)这因为xi不在(xj)A(xj)中出现，同上可证前式。故命题得证，即(xi)A(xi)～(xj)A(xj)。

2、公式代换定理

（1）定理：设公式A*中包含子公式A，把A*中的一处或多处A用B代换得到公式B*，

则①󰀀Cl(AB)(A* B*) ②若A～B，则A*～B*

③若(xi)A(xi)为A*的子公式，xi是A(xi)的自由变元，xj不在A(xi)中出现，记B*为A*中的(xi)A(xi)代换成(xj)A(xj)得到的公式，则

A*～B*

（2）注：这个定理不证了，因为②是①的推论，③是②和变元代换定理的推论，而①的证明要难一些，且要用到如下结论

70

①设AF，则A是定理ClA是定理。

②设A,BF,则󰀀(xi)(AB)((xi)A(xi)B)。

三、前束范式

有了可证等价和代换定理，我们就可以把每一个公式写成一种统一的规范形式，然后用这种规范形式就可以推出完备性了，这种规范的形式不仅为我们证明完备性提供了方便，更重要的是为我们证明公式是否为定理提供了一种机器自动证明的前提和便利，使得机器证明成为可能。

（一）一些必要的引理

1、 设xi不在A中自由出现，则(xi)(AB)～A(xi)B 2、设xi不在A中自由出现，则(xi)(AB)～A(xi)B 3、设xi不在A中自由出现，则(xi)(AB)～(xi)AB

4、设xi不在A中自由出现，则(xi)(AB)～(xi)AB

这四个引理是很重要也很有用的，它表明在可证等价的意义下可以把公式中间的量词移动公式前面去。

我们略去它们的证明，把证明的过程留给读者作为练习。

（二）前束范式的概念

1、 定义：设AF，若A具有以下形式

(Q1xi)„(Qnxin)D

1这里Qj(j=1,….,n)为或，D中不含量词，则称A为前束范式。 2、 例

（1）显然不含量词的公式也是前束范式，即n=0。 （2）(2( x1, x2) A1x3)(x1)(x4)(x5)(x2)((A11(

x3)) A22( x4, x5))为一个前束范式。

（3）原子公式是前束范式。

71

（4）不含连接词的公式是前束范式

（三）公式的前束范式存在性

1、前束范式存在定理：设 AF，则A可证等价于一个前束范式B，称B为A的一个前束范式。 证明：（1）由变元代换定理，可设A中所有的约束变元都互不相同，且都不同于A中的自由变元。

（2）用归纳法关于A中的连接词和量词的总个数归纳证明。

①若A不含连接词和量词，则A是原子公式，自然是前束范式。设A不是原子公式，且假定每个所含连接词和量词总数少于A的连接词和量词总数公式都可化为可证等价的前束范式。 ②分情况归纳证明

（i）设A是┐C，由归纳假设有前束范式C1～C，设C1为 (Q1xi)„(Qnxik)D，D不含量词

1 则A=┐C～┐C1 ～(Q1*xi1)„ (Qkxik) ┐D

这里Qj为或时，Qi*为或 ，得证A可证等价于前束范式。 （ii）设A=CD,由归纳假设

A～(Q1xi)„(Qnxik)C1 (R1yj)„(Rlyj)D1

11l 这里Qs，Rt为或，C1，D1不含量词，由假设xi1,„, xik不在(R1yj)„

1(Rlyjl)D1中自由出现，由引理3和4，可知

A～(Q1*xi1)„(Qkxik)(C1 (R1yj)„(Rlyjl)D1)

1* 这里Qs分别当Qs为或时为或，又yj,„,yjl不在C1中自由出现，由

1引理1和2，得A～(Q1*xi1)„(Qkxik)(R1yj)„(Rlyj)(C1

1lD1)

(iii)设A=(xi)C1

由归纳假设C可证等价于前束范式，所以A也可证等价于前束范式。

2、公式的前束范式求法：

这个求法，也是一种可以机器实现的算法：它是上述证明过程的算法实现。

第一步，约束变元换名，即所有的约束变元互不相同且与自由变元不同（变元代换）。 第二步，消去量词前的否定词“┐”，这时“┐”之后的量词都要改变，公式后边的公式变为否定。

72

第三步，量词前移，前项前移量词换，后项前移量不变。 3、 例

求下列公式的前束范式

（1）(2x2)A1( x2, x3)=A x1)A11(x1)  (解：第一步，已完成，

第二步，无否词，

第三步，由于x2不在( A～(x1)A11(x1) 中自由出现，所以由引理1

2A()x2)((x1)A1x111(x2,x3))，

21 又由于x1不在A A～((x2,x3)中自由出现，所以由引理4

2A()x2)(x1)(A1x111(x2,x3))。

即得前束范式。

注：由于算法第一步的完成，保证了引理1－引理4中的条件均被满足，故可以直接引用，以后不再一一标明条件被满足。

(2)A=((x1)(x2)A21(x1,x2

)┐(x2

)A11(x2

))

(x1)(x2)A22(x1,x2)

解：A～((x1)(x2)A21(x1,x2

)┐(x3

)A11(x3

))

(x4)(x5)A22(x4, x5)

～((x1

)(x2

)A21(x1,x2

)(x3

)┐A11(x3

))

(x4)(x5)A22(x4,x5)

～((x1

)(x2

)(x3

)(A21(x1,x2

)┐A11(x3

))

(x4)(x5)A22(x4,x5)

～(x1)(x2)(x3)(x4)(x5)((A21(x1,x2)┐A11(x3))

A22(x4, x5))

得前束范式。

4、 注意：在这个例子的第三步中我们首先在前一项中前移(x3)，再前移

(x1)(x2)，得到(x1)(x2)(x3)的顺序，其次，又先前移

73

(x4

)(x5

)，再前移(x1

)(x2

)(x3

)，得到

(x1)(x2)(x3)(x4)(x5)的顺序。

当然我们也可以得到：

A～(x5)(x4)(x3)(x2)(x1)((A21(x1, x2)┐A11(x3))

A22(x4,x5)

～(x3)(x1)(x2)(x4)(x5)((A21(x1,x2)┐A11(x3))

A22(x4,x5)

这表明一个公式前束范式是不唯一的，而这些形式中有的很简明，有的就不简明，原因就在于与在中间换了几次，这就引出了如下的概念。

（四）Π-型与Σ-前束范式

1、 定义：（1）以全称量词开头的前束范式称为Π-型前束范式，若此后量词符改变了n-1

次(n1)，则称该式为Πn-前型束范式。

（2）以存在量词开头的前束范式称为Σ-型前束范式，若此后量词符改变了n-1次

(n1)，则称该式为Σn-前型束范式。

2、 注：我们的目的是要化Σ型为Π型，以利于自动推理和定理机器证明，要做到这一点就

要用完备性定理了。

四、K的完备性定理

（一）项代入定理

定理：设A(xi)是含有自由变元xi的定理，则对任一项t，A(t)也是定理。

证明：由变元代换定理，可设A中约束变元均不在t中出现，这样t关于A(xi)中的xi是自由的，而A(xi)是定理，所以(xi)A(xi)也是定理，由(K5)和MP，即得A(t)是定理。

（二）完备性定理：设AF

我们略去它的证明。

，则󰀀A‘A

74

§4 Skolem标准形与Herbrand定理

（子句理论）

子句理论是自动推理与定理机器证明的基础，也是数理逻辑得以广泛应用的前提，它使谓词逻辑公式的定理证明机器化成为可能。

我们从已知A1,,An推证B，就是证明A1An󰀀B,用反证法就是证明

A1An┐B为矛盾式，我们的机器化证明，就是给出A1An┐B为矛盾式

的算法。

一、Skolem标准形

我们在上一节的前束范式中，已经证明任一个公式都可以化为一个与之可证等价的前束 范式。

(Q1x1)(Qnxn)D

n0,D不含量词

为了方便起见我们设公式中的全体自由变元为x1xn，Qi为或。由于Qi使，

可能交替出现，使得这种形式仍不够理想，我们的想法是能否消去前束范式中的量词，

这当然能保证等价最好，不能保证等价的话，如果能保证其它的某种等同关系也行，如同为矛盾式就是我们所需要的。这就是Skolem变形与求Skolem标准形的过程和目的。

（一）Skolem变形

1、 化去前束范式中Q1为的量词x1，即将

(x1)(Q2x2)(Qnxn)D(x1xn)= (x1)A(x1)

变形为(Q2x2)(Qnxn)D(c)=A(c)

x1)A(x1)化为

（1） 方法是：任选一个不在A中出现的个体常元c，则(A(c)，即在公式中直接去掉(x1)，将公式余下部分中x1处均换为c。

（2） 这时的A(c)与(x1)A(x1)一般不再可证等价，因为这里的c未必就是

x1 在解释的赋值中的值，但有如下的结论。

（3） 命题：将(x1)A(x1)化为A(c)，则(x1)A(x1)为矛盾式

75

A(c)为矛盾式。即：Skolem变形前后矛盾式的一致性。

证：“”设(的在任一个解释中任一个赋值均不满足x1)A(x1)为矛盾式，则£

(x1)A(x1)=┐(x1)┐A(x1) ，所以满足(x1)┐A(x1)，从而与v'-等价的任一个赋值v'满足┐A(则由项代入定理知v不满足A( “”（反证）若(值v满足(x1)，即不满足A(x1)，特别令v' (x1)=v(c),c)，A(c)为矛盾式。

在某一个解释中的一个赋x1)A(x1)不是矛盾式，则存在£

x1)A(x1)，由于c不在A(x1)中出现，所以把v(c) 任意改变都不

影响v满足(x1)A(x1)，从而v不满足(x1)┐A(x1)，当然就有v'-等价的

x1)，v'满足A(x1)，这样我们设v(c) = v'(x1),仍由项代c)，与A(c)为矛盾式相矛盾。

赋值v'不满足┐A(入定理知v满足A(（4） 这样就保证了一个公式在删去第一个为的前束范式中的(公式与原公式同为矛盾式时的一致性。

x1)得到的新

2、化去某一个Qi＋1(i1)为而Q1,,Qi均为的前束范式中的量词(xi1)，这时的前束范式为(记为(x1)(xi－1)(xi)(xi＋1)(Qnxn)D(x1,,xn)，简

x1)(xi)(xi＋1)A(x1,,xi,xi1),x1,,xi1为A中的自由变元。

i（1）方法：任选一个不在A中出现的i元函数符号f，将公式化为 (

ix1)(xi)A(x1,,xi,fi(x1,,xi))

这里的f称为Skolem函数。

i（2） 变形后的公式与原公式也不一定可证等价，这因为在一个解释的赋值中f(x1,

,xi)的值未必就是xi＋1在这赋值中对应的值。

（3） 命题(x1)(xi)(xi＋

1

)A(x1,,xi1)为矛盾式

(x1)(xi)A(x1,,xi,fi(x1,,xi))为矛盾式。

76