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

1、第七章 可靠性和完全性（提綱）1. 可靠性與完全性現(xiàn)在邏輯基本上都是采用如下結(jié)構(gòu)：形式語言語義 語法語義與語法的關(guān)系形式語言：從初始符號出發(fā)，形成主要對象公式。（可能需要一些其它輔助對象，如在一階邏輯，就有項的概念）。公式是一種特殊的符號串（由初始符號組成的符號串）。語義：給出某種結(jié)構(gòu)，通過某種定義，定義出刻畫邏輯規(guī)律的有效式。（如在一階邏輯，我們從結(jié)構(gòu)和賦值出發(fā)，給出解釋、公式在解釋下的真值，用在所有解釋下都真定義出有效式）。有效式是一種特殊的公式，所有有效式的集合是全體公式的一個子集。語法：由公理和推導(dǎo)規(guī)則組成。按某種標(biāo)準(zhǔn)的方法給出證明序列和內(nèi)定理。（可以有一些推廣的概念，最重要的是推演）

2、。有效式是一種特殊的公式，所有內(nèi)定理的集合是全體公式的一個子集。語義與語法的關(guān)系：最重要的有兩個，可靠性和完全性。7.1.1定義 可靠性 所有的內(nèi)定理都是有效式。7.1.2定義 完全性 所有的有效式都是內(nèi)定理。2. 一階推演系統(tǒng)的可靠性可靠性有標(biāo)準(zhǔn)的證明方法：1. 證明每個公理都是有效的。2. 證明推導(dǎo)規(guī)則保持有效性不變。3. 歸納證明證明序列中的每個公式都是有效式，所以內(nèi)定理是有效式。7.2.1引理(1) s(j®y) = T當(dāng)且僅當(dāng)（如果s(j) = T，則s(y) = T）。(2) s(j1®®jn®y) = T 當(dāng)且僅當(dāng)（如果s(j1) = T,

3、 , s(jn) = T，則s(y) = T）。證 (1) 由定義得s(j®y) = T當(dāng)且僅當(dāng) s(j) = F或s(y) = T。s(j) = F或s(y) = T就是（如果s(j) = T，則s(y) = T）。所以，s(j®y) = T當(dāng)且僅當(dāng)（如果s(j) = T，則s(y) = T）。(2) 對n作歸納。1. n = 1。由(1)得s(j1®y) = T 當(dāng)且僅當(dāng)（如果s(j1) = T，則s(y) = T）。2. n = k+1。j1®®jk+1®y也就是j1®®jk®(jk+1®

4、y)，由歸納假設(shè)s(j1®®jk®(jk+1®y) = T 當(dāng)且僅當(dāng)（如果s(j1) = T, , s(jk) = T，則s(jk+1®y) = T）。由(1)得s(jk+1®y) = T 當(dāng)且僅當(dāng)（如果s(j k+1) = T，則s(y) = T）。所以，s(j1®®jn®y) = T 當(dāng)且僅當(dāng)（如果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定理 一階推演系統(tǒng)的公理都是有效式。證A1 j®y®j。任給解釋s，如果s(j) = T, s(y) = T，則s(j) = T。由定理(2)，任給解釋s，都有s(j®y®j) = T。A2 (j®y®q)®(j®y)®j®q。任給解釋s，如果s(j®y®q) = T, s(j®y) = T

6、, 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。由定理(2)，任給解釋s，都有s(j®y®q)®(j®y)®j®q) = T。A3 (Øj®y)®(Øj®Øy)®j任給解釋s，如果s(Øj®y) = T, s(Øj®

7、;Øy) = T，則用反證法證明s(j) = T。假設(shè)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，矛盾。由定理(2)，任給解釋s，都有s(Øj®y)®(Øj®Øy)®j) = T。A4 "xj®j(t / x)，在j中t對x

8、代入自由。任給解釋s，如果s("xj) = T，則任給aÎA，都有sx, a(j) = T，取a = s(t)，由代入引理得s(j(t / x) = sx, a(j) = T。由定理(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, a(j) = T，所以任給aÎ

9、A，都有sx, a(y) = T，因此s("xy) = T。由定理(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。由定理(2)，任給解釋s，都有s(j®"xj) = T。7.2.4定理 一階推演系統(tǒng)的推導(dǎo)規(guī)則保持有效性不變。(1) 如果j®y和j都是有效式，則y也是有效式

10、。(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定理 一階推演系統(tǒng)可靠性定理一階推演系統(tǒng)的內(nèi)定理都是有效式。證 設(shè)j是內(nèi)定理，j1, , jn（=j）是它的證明序列，歸納證明任

11、給k（1£k£n），jk都是有效式，當(dāng)k = n時，就是說j是有效式。1. ji是公理，由定理得ji是有效式。2.1 存在j, k<i£n，使得jk = jj®ji。由歸納假設(shè)得jj和jk = jj®ji都是有效式，由定理(1)得ji是有效式。2.2 存在j<i，存在變項x，使得ji = "x jj。由歸納假設(shè)得jj是有效式，由定理(2)得ji = "x jj是有效式。7.2.6補充 A7和A8是有效式。證A7 t º t。任給解釋s，如果s(t) = s(t)，所以s(t º t)。A8 t

12、 º 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。由定理(2)，任給解釋s，都有s( t º s®(j(t / x)®j(s / x) = T。7.2.7補充 帶等詞的一階推演系統(tǒng)可靠性定理帶等詞的一階推演系統(tǒng)的內(nèi)定理都是有效式。證 略。3. 和諧和極大和諧7.3.1定義 和諧 F是公式集。如果存在公式

13、j，使得F | j且F | Øj，則稱F是不和諧的。否則稱F是和諧的。由定義，F(xiàn)是和諧的條件是：不存在公式j(luò)，使得F | j且F | Øj。7.3.2定理 和諧集等價條件(1) F是不和諧的 當(dāng)且僅當(dāng)（任給公式q，都有F | q）。(2) F是和諧的 當(dāng)且僅當(dāng)（存在公式q，使得F |/ q）。證 (1) 如果（任給公式q，都有F | q），當(dāng)然存在公式j(luò)，使得F | j且F | Øj。如果存在公式j(luò)，使得F | j且F | Øj，則任給公式q，由j, Øj | q得F | q。(2) 由(1)直接可得。7.3.3定理 和諧集的性質(zhì)(1) 單調(diào)性

14、 F Í Y。如果F是不和諧，則Y也是不和諧的。所以如果Y是和諧的，則F也是和諧的。(2) 有限性 F是和諧的 當(dāng)且僅當(dāng) F的每個有限子集是和諧的。(3) F |/ j 當(dāng)且僅當(dāng) FÈØj是和諧的。(4) F |/ Øj 當(dāng)且僅當(dāng) FÈj是和諧的。證 (1) 如果F是不和諧，則任給公式q，都有F | q，所以任給公式q，都有Y | q，因此Y是不和諧的。(2) 證明：F是不和諧的 當(dāng)且僅當(dāng) 存在F的有限子集Y是不和諧的。設(shè)F是不和諧的，則存在公式j(luò)，使得F | j且F | Øj。取F到j(luò)的推演序列為j1, , jn，令F1 = j1,

15、 , jnÇF，則F1是F的有限子集且F1 | j，類似地存在有限F的有限子集F2，使得F2 | Øj。所以存在F的有限子集Y = F1ÈF2，使得Y | j且Y |Øj，因此存在F的有限子集Y，使得Y是不和諧的。設(shè)存在F的有限子集Y是不和諧的，由單調(diào)性得F是不和諧的。(3) 證明：F | j 當(dāng)且僅當(dāng) FÈØj是不和諧的。設(shè)F | j，則FÈØj | j，又FÈØj | Øj，所以FÈØj是不和諧的。設(shè)FÈØj是不和諧的，則FÈ

16、16;j | j，由演繹定理得F | Øj®j，由Øj®j | j得F | j。(4) 類似于(3)，留給讀者。7.3.4定義 極大和諧 F是和諧的公式集。如果任給公式j(luò)ÏF，都有FÈj是不和諧的，則稱F是極大和諧的。7.3.5定理 極大和諧集的性質(zhì) F是極大和諧的公式集。(1) 推演封閉性 如果F | j，則jÎF。(2) 內(nèi)定理封閉性 如果j是內(nèi)定理，則jÎF。(3) 分離規(guī)則 如果jÎF且j®yÎF，則yÎF。(4) ØjÎF 當(dāng)且僅當(dāng) jÏ

17、;F。(5) j®yÎF 當(dāng)且僅當(dāng) jÏF或yÎF。證 (1) 反證法。如果jÏF，則FÈj是不和諧的，由定理(4)得F | Øj，又F | j，所以F是不和諧的，矛盾。(2) 如果j是內(nèi)定理，則由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ÏF。jÎF如果jÏF，則FÈj是不和諧的，由定理(4)得F | 

18、16;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®(j®y)是內(nèi)定理，所以Øj®(j®y)ÎF，再由(3)得j

19、®yÎF。情況2，yÎF。類似情況1，由內(nèi)定理y®(j®y)。由(4)和(5)得：(4¢) ØjÏF 當(dāng)且僅當(dāng) jÎF。(5¢) j®yÏF 當(dāng)且僅當(dāng) jÎF且yÏF。7.3.6推論 F是極大和諧的公式集。(1) jÙyÎF 當(dāng)且僅當(dāng) jÎF且yÎF。(2) jÚyÎF 當(dāng)且僅當(dāng) jÎF或yÎF。證 (1) jÙyÎF 當(dāng)且僅當(dāng) Ø(j®

20、Øy)ÎF 當(dāng)且僅當(dāng) j®ØyÏF 當(dāng)且僅當(dāng) jÎF且ØyÏF 當(dāng)且僅當(dāng) jÎF且yÎF。(2) jÚyÎF 當(dāng)且僅當(dāng) Øj®yÎF 當(dāng)且僅當(dāng) ØjÏF或yÎF 當(dāng)且僅當(dāng) jÎF或yÎF。4. Hintikka集7.4.1定義 Hintikka集 F是公式集。如果任給存在公式$xyÎF，都存在項t，使得y(t/x)ÎF，則稱F是Hintikka集。7.4.2定理 極大和諧Hin

21、tikka集存在定理F是有限公式集，則存在極大和諧的Hintikka集Y，使得F Í Y。證 注意，我們的語言是可數(shù)的，所以全體公式也是可數(shù)的，將全體公式排成序列：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 = $xy。取不在FkÈjk出現(xiàn)的變元y（這是可以做到的，因為FkÈjk是有限公式集），令Fk+1 = (

22、FkÈjk)Èy(y/x)。令Y =Fn | nÎN。證明一：每個Fn都是和諧的。(1) F0 = F是和諧的。(2) Fk+1分三種情況證明如下：2.1 FkÈjk不和諧。由歸納假設(shè)，F(xiàn)k是和諧的，所以Fk+1 = Fk是和諧的。2.2 FkÈjk和諧。令Fk+1 = FkÈjk和諧的。2.3 FkÈjk和諧，jk = $xy。反證法。假設(shè)Fk+1 = (FkÈjk)Èy(y/x)是不和諧的，則FkÈjk | Øy(y/x)。由概括規(guī)則得FkÈjk | "y

23、16;y(y/x)（注意y不是FkÈjk的自由變項）。由內(nèi)定理 | "yØy(y/x)«"xØy得"yØy(y/x) | "xØy，所以FkÈjk | "xØy由內(nèi)定理 | "xØy«Ø$xy 得"xØy | Ø$xy，所以FkÈjk | "xØy。這就是FkÈjk | Øjk，由演繹定理得Fk | jk®Øjk。再由內(nèi)定理 |

24、 (jk®Øjk)®Øjk得jk®Øjk | Øjk，所以Fk | Øjk，因此FkÈjk不和諧，矛盾。證明二：Fn Í Fn+1，所以Fn | nÎN是單調(diào)的。顯然。證明三：Y =Fn | nÎN是和諧的。反證法。如果Y =Fn | nÎN是不和諧的，則存在Y的有限子集y1, , ys，存在公式q使得y1, , ys | qÙØq。因為y1, , ys ÍFn | nÎN，所以存在Fn1, , Fns，使得y1ÎF

25、n1, , ysÎFns，取Fn1, , Fns中最大的集合Fnt（這個最大集合的存在是由Fn | nÎN的單調(diào)性保證的），則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. 一階推演系統(tǒng)的完全性7.5.1定義 可滿足(1) j是公式。如果存在解釋s，使得s(j) = T，則稱j是可滿足的。(2) F是公式集。如果存在解釋s，使得任給公式j(luò)ÎF，都有s(j) = T，則稱F是可滿足的，記為s(F) = T。7.5.2引理(1) Øj可滿足 當(dāng)且僅當(dāng) j不是有效的。(2) F是公式集。如果F可滿足，則任給公式j(luò)ÎF，j都是可滿足的。證 略。注意，任給公式j(luò)Î