高级数理逻辑第五章第六章.pptVIP

紧致性定理 ∑?Form(L )可满足 当且仅当 ∑的任何有限子集可满足。 证：必要性。显然。 充分性。假设∑不可满足。由完备性， ∑不协调，即存在A∈ Form(L )，使得∑├A且∑├?A。进一步得到，存在有限∑0， ∑1 ?∑，使得∑0├A，∑1├?A。可得∑0，∑1├A且∑0，∑1├?A。即有限集∑0∪∑1不协调。由可靠性， ∑0∪∑1不可满足。（矛盾） L-S定理 设∑?Form(L )，则 对于不含相等符号的∑， ∑可满足 iff ∑在可数无限论域中可满足。 对于含相等符号的∑， ∑可满足 iff ∑在可数无限论域或某个有限论域中可满足。 无?前束范式 设A为前束范式，使用以下规则变换得到的公式A’为A的无?前束范式。 若?y的左面没有全称量词，则u代入y，且删掉?y，其中u不在A和每个步骤中出现。 若?y的左面所有全称量词为?x1，?x2，…，?xn，则f(x1, x2, …, xn)代入y，且删掉?y，其中f不在A和每个步骤中出现。 例子 A=?y1?y2?x1?y3?x2?x3?y4?y5?x4 B(y1, y2, x1, y3, x2, x3, y4, y5, x4) A’=?x1?x2?x3?x4 B(u, v, x1, f(x1), x2, x3, g(x1, x2, x3), h(x1, x2, x3), x4) 定理 前束范式A在论域D中是可满足的 当且仅当 它的无?前束范式在D中是可满足的。因此，A可满足 当且仅当 它的无?前束范式可满足。 证：不失一般性。设A=?x?y?zB(x, y, z)，其无?前束范式A’=?yB(u, y, f(y))。 A在D上可满足 iff ?y?zB(u, y, z)在D上可满足 ? iff ?yB(u, y, f(y))在D上可满足 必要性（一） 由?y?zB(u, y, z)在D上可满足，则存在D上赋值v，使得?y?zB(u, y, z)v=1，即对于任何α∈D， ?zB(u, u1, z)v(u1/α)=1。存在β∈D，使得B(u, u1, u2)v(u1/α)(u2/β)=1。 其中u1，u2不在B(u, y, z)中出现。 令v’是D上的赋值，且除fv’(α)= β外，其余都与v相同。则 f(u1)v’(u1/α) = fv’(u1/α) (u1v’(u1/α)) =fv’(α)=u2v(u1/α)(u2/β) 必要性（二） 由B(u, u1, u2)v(u1/α)(u2/β)=1，可得 uv(u1/α)(u2/β), u1v(u1/α)(u2/β), u2v(u1/α)(u2/β) ∈Bv(u1/α)(u2/β)。 进而可得 uv’(u1/α), u1v’(u1/α), f(u1)v’(u1/α) ∈Bv’(u1/α)。 因此，B(u, u1, f(u1))v’(u1/α)=1。 ?yB(u, y, f(y))v’=1。 充分性（一） 由?yB(u, y, f(y))在D上可满足，则存在D上赋值v，使得?yB(u, y, f(y))v=1，即对于任何α∈D， B(u, u1, f(u1))v(u1/α)=1，其中u1不在B(u, y, f(y))中出现。 β=fv(α) ∈D f(u1)v(u1/α) = fv(u1/α) (u1v(u1/α)) =fv(α)=u2v(u1/α)(u2/β)，其中u2不在B(u, u1, f(u1))中出现。 充分性（二） 由B(u, u1, f(u1))v(u1/α)=1，可得 uv(u1/α), u1v(u1/α), f(u1)v(u1/α) ∈Bv(u1/α)。 进而可得 uv(u1/α)(u2/β), u1v(u1/α)(u2/β), u2v(u1/α)(u2/β) ∈Bv(u1/α)(u2/β)。 因此，B(u, u1, u2)v(u1/α)(u2/β)=1。 ?zB(u, u1, z)v(u1/α)=1。 ?y?zB(u, y, z)v=1。 Herbrand域 定义： 设A∈Form(L )为无?前束范式，称{t’|t由A中出现的个体符号，自由变元符号和函数符号所生成的项（若A中无个体符号、自由变元符号，则取任一个自由变元符号）}为Herbrand域，记为HA或H。 例子 A=?x(F(u)∧F(b)∧F(f(x))) HA={u, b, f(u), f(b), f(f(u)), f(f(b)),…} B=?xF(f(x)) HB={u, f(u), f(f(u)),…} Herbrand赋值 定义：设A