紧致性定理.ppt

L-S定理无∃前束范式例子定理必要性（一）必要性（二）充分性（一）充分性（二）Herbrand域例子Herbrand赋值定理1.若A为原子公式，则Av=Av’=1。
2.若A不含全称量词，则Av=Av’=1。
3.若A含全称量词，则
不失一般性，令A=∀xB(x)，B(x)中不含量词。
对于任何t’∈HA，由于tv’∈D且∀xB(x)v’=1，B(u)v’(u/tv’)=1。
B(u)v(u/t’)=B(u)v(u/tv)=B(t)v=B(t)v’=B(u)v’(u/tv’)=1。
所以，矛盾。例式Herbrand定理必要性充分性判定A1，A2，…，An├A是否成立公理推理系统(Ax9)(A→C)→((B→C)→(A∨B→C))
(Ax10)(A↔B)→(A→B)
(Ax11)(A↔B)→(B→A)
(Ax12)(A→B)→((B→A)→(A↔B))
(Ax13)∀xA(x)→A(t)
(Ax14)∀x(A→B(x))→(A→∀xB(x))，x不在A中出现
(Ax15)A(t)→∃xA(x)，其中A(x)是在A(t)中把t的某些（不一定全部）出现替换成x而得。
(Ax16)∀x(A(x)→B)→(∃xA(x)→B)，x不在B中出现
(Ax17)t1≡t2→(A(t1)→A(t2))，其中A(t2)是在A(t1)中把t1的某些（不一定全部）出现替换成t2而得。
(Ax18)u≡u
推演规则
(R1)由A→B和A推出B。
(R2)由A(u)推出∀xA(x)。∑├zA例子Ф├z(B→C)→((A→B)→(A→C))
证：
(1)((A→(B→C))→((A→B)→(A→C)))→((B→C)→((A→(B→C))→((A→B)→(A→C))))
(Ax1)
(2)(A→(B→C))→((A→B)→(A→C))
(Ax2)
(3)(B→C)→((A→(B→C))→((A→B)→(A→C)))
(R1)(1)(2)
(4)((B→C)→((A→(B→C))→((A→B)→(A→C))))→
(((B→C)→(A→(B→C)))→
((B→C)→((A→B)→(A→C))))
(Ax2)
(5)((B→C)→(A→(B→C)))→((B→C)→((A→B)→(A→C)))
(R1)(3)(4)
(6)(B→C)→(A→(B→C))(Ax1)
(7)(B→C)→((A→B)→(A→C))
(R1)(5)(6)自然推理系统与公理推理系统的关系