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