第七章 可靠性和完全性(提纲)

1、第七章 可靠性和完全性（提纲）1. 可靠性与完全性现在逻辑基本上都是采用如下结构：形式语言语义 语法语义与语法的关系形式语言：从初始符号出发，形成主要对象公式。（可能需要一些其它辅助对象，如在一阶逻辑，就有项的概念）。公式是一种特殊的符号串（由初始符号组成的符号串）。语义：给出某种结构，通过某种定义，定义出刻画逻辑规律的有效式。（如在一阶逻辑，我们从结构和赋值出发，给出解释、公式在解释下的真值，用在所有解释下都真定义出有效式）。有效式是一种特殊的公式，所有有效式的集合是全体公式的一个子集。语法：由公理和推导规则组成。按某种标准的方法给出证明序列和内定理。（可以有一些推广的概念，最重要的是推演）

2、。有效式是一种特殊的公式，所有内定理的集合是全体公式的一个子集。语义与语法的关系：最重要的有两个，可靠性和完全性。7.1.1定义 可靠性 所有的内定理都是有效式。7.1.2定义 完全性 所有的有效式都是内定理。2. 一阶推演系统的可靠性可靠性有标准的证明方法：1. 证明每个公理都是有效的。2. 证明推导规则保持有效性不变。3. 归纳证明证明序列中的每个公式都是有效式，所以内定理是有效式。7.2.1引理(1) s(j®y) = T当且仅当（如果s(j) = T，则s(y) = T）。(2) s(j1®®jn®y) = T 当且仅当（如果s(j1) = T,

3、 , s(jn) = T，则s(y) = T）。证 (1) 由定义得s(j®y) = T当且仅当 s(j) = F或s(y) = T。s(j) = F或s(y) = T就是（如果s(j) = T，则s(y) = T）。所以，s(j®y) = T当且仅当（如果s(j) = T，则s(y) = T）。(2) 对n作归纳。1. n = 1。由(1)得s(j1®y) = T 当且仅当（如果s(j1) = T，则s(y) = T）。2. n = k+1。j1®®jk+1®y也就是j1®®jk®(jk+1®

4、y)，由归纳假设s(j1®®jk®(jk+1®y) = T 当且仅当（如果s(j1) = T, , s(jk) = T，则s(jk+1®y) = T）。由(1)得s(jk+1®y) = T 当且仅当（如果s(j k+1) = T，则s(y) = T）。所以，s(j1®®jn®y) = T 当且仅当（如果s(j1) = T, , s(jn) = T，则s(y) = T）。7.2.2引理(1) 如果s(j®y) = T且s(j) = T，则s(y) = T。(2) 如果s(j®y) = T

5、且s(j) = T，则s(y) = T。证 (1) 如果s(j®y) = T，则s(j) = F或s(y) = T，又s(j) = T，所以s(y) = T。7.2.3定理 一阶推演系统的公理都是有效式。证A1 j®y®j。任给解释s，如果s(j) = T, s(y) = T，则s(j) = T。由定理7.2.1(2)，任给解释s，都有s(j®y®j) = T。A2 (j®y®q)®(j®y)®j®q。任给解释s，如果s(j®y®q) = T, s(j®y

6、) = T, s(j) = T，则由s(j) = T和s(j®y®q) = T得s(y®q) = T，由s(j) = T和s(j®y) = T得s(y) = T，再由s(y) = T和s(y®q) = T得s(q) = T。由定理7.2.1(2)，任给解释s，都有s(j®y®q)®(j®y)®j®q) = T。A3 (Øj®y)®(Øj®Øy)®j任给解释s，如果s(Øj®y) = T, s(&#

7、216;j®Øy) = T，则用反证法证明s(j) = T。假设s(j) = F，则s(Øj) = T，由s(Øj) = T和s(Øj®y) = T得s(y) = T，由s(Øj) = T和s(Øj®Øy) = T得s(Øy) = T，所以s(y) = F。s(y) = T和s(y) = F，矛盾。由定理7.2.1(2)，任给解释s，都有s(Øj®y)®(Øj®Øy)®j) = T。A4 "xj®

8、j(t / x)，在j中t对x代入自由。任给解释s，如果s("xj) = T，则任给aÎA，都有sx, a(j) = T，取a = s(t)，由代入引理得s(j(t / x) = sx, a(j) = T。由定理7.2.1(2)，任给解释s，都有s("xj®j(t / x) = T。A5 "x(j®y)®("xj®"xy)。任给解释s，如果s("x(j®y) = T, s("xj) = T，则任给aÎA，都有sx, a(j®y) = T且sx,

9、a(j) = T，所以任给aÎA，都有sx, a(y) = T，因此s("xy) = T。由定理7.2.1(2)，任给解释s，都有s("x(j®y)®("xj®"xy) = T。A6 j®"xj，x不是j的自由变项。任给解释s，如果s(j) = T，则任给aÎA，由合同引理得sx, a(j) = s(j) = T，所以s("xj) = T。由定理7.2.1(2)，任给解释s，都有s(j®"xj) = T。7.2.4定理 一阶推演系统的推导规则保持有效性不变

10、。(1) 如果j®y和j都是有效式，则y也是有效式。(2) 如果j是有效式，则"xj也是有效式。证(1) 任给解释s，因为j®y和j都是有效式，所以s(j®y) = T且s(j) = T，因此s(y) = T。这就证明了任给解释s，都有s(y) = T，所以y是有效式。(2) 任给解释s，任给aÎA，因为j是有效式，所以sx, a(j) = T，因此s("xj) = T。这就证明了任给解释s，都有s("xj) = T，所以"xj是有效式。7.2.5定理 一阶推演系统可靠性定理一阶推演系统的内定理都是有效式。证 设j

11、是内定理，j1, , jn（=j）是它的证明序列，归纳证明任给k（1£k£n），jk都是有效式，当k = n时，就是说j是有效式。1. ji是公理，由定理7.2.3得ji是有效式。2.1 存在j, k<i£n，使得jk = jj®ji。由归纳假设得jj和jk = jj®ji都是有效式，由定理7.2.4(1)得ji是有效式。2.2 存在j<i，存在变项x，使得ji = "x jj。由归纳假设得jj是有效式，由定理7.2.4(2)得ji = "x jj是有效式。7.2.6补充 A7和A8是有效式。证A7 t 

12、6; t。任给解释s，如果s(t) = s(t)，所以s(t º t)。A8 t º s®(j(t / x)®j(s / x)。任给解释s，如果s( t º s) = T, s(j(t / x) = T，则s(t) = s(s)，取a = s(t) = s(s)，则由代入引理得s(j(s / x) = sx, a(j) = s(j(t / x) = T。由定理7.2.1(2)，任给解释s，都有s( t º s®(j(t / x)®j(s / x) = T。7.2.7补充 带等词的一阶推演系统可靠性定理带等词的一阶推

13、演系统的内定理都是有效式。证 略。3. 和谐和极大和谐7.3.1定义 和谐 F是公式集。如果存在公式j，使得F | j且F | Øj，则称F是不和谐的。否则称F是和谐的。由定义，F是和谐的条件是：不存在公式j，使得F | j且F | Øj。7.3.2定理 和谐集等价条件(1) F是不和谐的 当且仅当（任给公式q，都有F | q）。(2) F是和谐的 当且仅当（存在公式q，使得F |/ q）。证 (1) 如果（任给公式q，都有F | q），当然存在公式j，使得F | j且F | Øj。如果存在公式j，使得F | j且F | Øj，则任给公式q，由j, &#

14、216;j | q得F | q。(2) 由(1)直接可得。7.3.3定理 和谐集的性质(1) 单调性 F Í Y。如果F是不和谐，则Y也是不和谐的。所以如果Y是和谐的，则F也是和谐的。(2) 有限性 F是和谐的 当且仅当 F的每个有限子集是和谐的。(3) F |/ j 当且仅当 FÈØj是和谐的。(4) F |/ Øj 当且仅当 FÈj是和谐的。证 (1) 如果F是不和谐，则任给公式q，都有F | q，所以任给公式q，都有Y | q，因此Y是不和谐的。(2) 证明：F是不和谐的 当且仅当 存在F的有限子集Y是不和谐的。设F是不和谐的，则存在公式

15、j，使得F | j且F | Øj。取F到j的推演序列为j1, , jn，令F1 = j1, , jnÇF，则F1是F的有限子集且F1 | j，类似地存在有限F的有限子集F2，使得F2 | Øj。所以存在F的有限子集Y = F1ÈF2，使得Y | j且Y |Øj，因此存在F的有限子集Y，使得Y是不和谐的。设存在F的有限子集Y是不和谐的，由单调性得F是不和谐的。(3) 证明：F | j 当且仅当 FÈØj是不和谐的。设F | j，则FÈØj | j，又FÈØj | Øj，所以F&

16、#200;Øj是不和谐的。设FÈØj是不和谐的，则FÈØj | j，由演绎定理得F | Øj®j，由Øj®j | j得F | j。(4) 类似于(3)，留给读者。7.3.4定义 极大和谐 F是和谐的公式集。如果任给公式jÏF，都有FÈj是不和谐的，则称F是极大和谐的。7.3.5定理 极大和谐集的性质 F是极大和谐的公式集。(1) 推演封闭性 如果F | j，则jÎF。(2) 内定理封闭性 如果j是内定理，则jÎF。(3) 分离规则 如果jÎF且j®

17、;yÎF，则yÎF。(4) ØjÎF 当且仅当 jÏF。(5) j®yÎF 当且仅当 jÏF或yÎF。证 (1) 反证法。如果jÏF，则FÈj是不和谐的，由定理7.3.3(4)得F | Øj，又F | j，所以F是不和谐的，矛盾。(2) 如果j是内定理，则由5.3.1(1)得F | j，由(1)得jÎF。(3) 如果jÎF且j®yÎF，则F | y，由(1)得yÎF。(4) 如果ØjÎF，由F的和谐性得j&

18、#207;F。jÎF如果jÏF，则FÈj是不和谐的，由定理7.3.3(4)得F | Øj，由(1)得ØjÎF。(5) 如果j®yÎF，分两种情况证明jÏF或yÎF。情况1，jÏF。显然有jÏF或yÎF。情况2，jÎF。由(3)得yÎF，也有jÏF或yÎF。如果jÏF或yÎF，则分两种情况证明j®yÎF。情况1，jÏF。由(4)得ØjÎF，因为Øj&

19、#174;(j®y)是内定理，所以Øj®(j®y)ÎF，再由(3)得j®yÎF。情况2，yÎF。类似情况1，由内定理y®(j®y)。由(4)和(5)得：(4¢) ØjÏF 当且仅当 jÎF。(5¢) j®yÏF 当且仅当 jÎF且yÏF。7.3.6推论 F是极大和谐的公式集。(1) jÙyÎF 当且仅当 jÎF且yÎF。(2) jÚyÎF 当且仅当

20、 jÎF或yÎF。证 (1) jÙyÎF 当且仅当 Ø(j®Øy)ÎF 当且仅当 j®ØyÏF 当且仅当 jÎF且ØyÏF 当且仅当 jÎF且yÎF。(2) jÚyÎF 当且仅当 Øj®yÎF 当且仅当 ØjÏF或yÎF 当且仅当 jÎF或yÎF。4. Hintikka集7.4.1定义 Hintikka集 F是公式集。如果任给存在公式$x

21、yÎF，都存在项t，使得y(t/x)ÎF，则称F是Hintikka集。7.4.2定理 极大和谐Hintikka集存在定理F是有限公式集，则存在极大和谐的Hintikka集Y，使得F Í Y。证 注意，我们的语言是可数的，所以全体公式也是可数的，将全体公式排成序列：j1, , jn, ，任给n，归纳定义有限Fn如下：(1) F0 = F。(2) Fk+1分三种情况定义如下：2.1 FkÈjk不和谐。令Fk+1 = Fk。2.2 FkÈjk和谐，jk不是$xy形式。令Fk+1 = FkÈjk。2.3 FkÈjk和谐，jk = $

22、xy。取不在FkÈjk出现的变元y（这是可以做到的，因为FkÈjk是有限公式集），令Fk+1 = (FkÈjk)Èy(y/x)。令Y =Fn | nÎN。证明一：每个Fn都是和谐的。(1) F0 = F是和谐的。(2) Fk+1分三种情况证明如下：2.1 FkÈjk不和谐。由归纳假设，Fk是和谐的，所以Fk+1 = Fk是和谐的。2.2 FkÈjk和谐。令Fk+1 = FkÈjk和谐的。2.3 FkÈjk和谐，jk = $xy。反证法。假设Fk+1 = (FkÈjk)Èy(y/x)是不

23、和谐的，则FkÈjk | Øy(y/x)。由概括规则得FkÈjk | "yØy(y/x)（注意y不是FkÈjk的自由变项）。由内定理 | "yØy(y/x)«"xØy得"yØy(y/x) | "xØy，所以FkÈjk | "xØy由内定理 | "xØy«Ø$xy 得"xØy | Ø$xy，所以FkÈjk | "xØy。

24、这就是FkÈjk | Øjk，由演绎定理得Fk | jk®Øjk。再由内定理 | (jk®Øjk)®Øjk得jk®Øjk | Øjk，所以Fk | Øjk，因此FkÈjk不和谐，矛盾。证明二：Fn Í Fn+1，所以Fn | nÎN是单调的。显然。证明三：Y =Fn | nÎN是和谐的。反证法。如果Y =Fn | nÎN是不和谐的，则存在Y的有限子集y1, , ys，存在公式q使得y1, , ys | qÙØ

25、;q。因为y1, , ys ÍFn | nÎN，所以存在Fn1, , Fns，使得y1ÎFn1, , ysÎFns，取Fn1, , Fns中最大的集合Fnt（这个最大集合的存在是由Fn | nÎN的单调性保证的），则y1, , ys Í Fnt，所以Fnt | qÙØq，因此Fnt不和谐，矛盾。证明四：Y =Fn | nÎNHintikka集。任给存在公式$xyÎY，$xy一定是某个jn，因为YÈjn = Y和谐，所以FnÈjn和谐（注意FnÈjn是YÈjn的子集）。由定义2.3，存在变项y，使得y(y/x)ÎFn+1。所以，存在变项y，使得y(y/x)ÎY。5. 一阶推演系统的完全性7.5.1定义 可满足(1) j是公式。如果存在解释s，使得s(j) = T，则称j是可满足的。(2) F是公式集。如果存在解释s，使得任给公式jÎF，都有s(j) = T，则称F是可满足的，记为s(F) = T。7.5.2引理(1) Øj可满足 当且仅当 j不是有效的。(2) F是公式集。如果F可满足，则任给公式jÎF，j都是可满足的。证 略。注意，任给公式jÎF，j都是可满足的，并不保证F是可满足的