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。