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是可滿足的