高級數(shù)理邏輯第5講

1、4.5 一階謂詞語義系統(tǒng)4.5.1 什么是形式系統(tǒng)語義抽象公理系統(tǒng)或者形式系統(tǒng)，具有較高的抽象性。因此，已經(jīng)脫離了任何一個具體的系統(tǒng)，但是我們可以對形式系統(tǒng)作出各種解釋。通過這種解釋將形式系統(tǒng)對應到各種具體的系統(tǒng)中取。例如可以將一階謂詞邏輯系統(tǒng)，解釋到平面幾何系統(tǒng)中。怎樣將形式系統(tǒng)解釋成具體系統(tǒng)呢？我們先看下面的例子：如果我們要知道的具體的真值=1，我們至少要知道以下事情：1、 x在什么范圍之內(nèi)，x范圍是實數(shù)。2、 f是什么？ (X+1)3、 P是什么？P代表的是大于04、 a=？a=15、 x=?，x5，4例如，我們可以作出以下解釋：1、解釋1：l x在實數(shù)中取值l P表示等于0l 表示x-

2、al a=5因此，公式解釋為。令x=5, 則s(x) ->5s(f(a,x) ->I(f)(I(a),s(x)令x=6，則2、解釋2：l x在實數(shù)中取值l P表示大于等于0l 表示因此，公式解釋為。這個公式不必對a和x作出具體解釋，就可以確定公式的真值。即對于任何實數(shù)x，和賦值映射v，。由上面的例子可以看出，要對形式系統(tǒng)作出解釋，我們要了解以下問題：ü x取值于哪里？即規(guī)定討論問題的領(lǐng)域。ü 給出謂詞的含義和謂詞的真值ü 給出函數(shù)的解釋ü 給出變量和常量的值ü 根據(jù)連接詞的賦值規(guī)則，賦值這就是我們要研究的語義系統(tǒng)指稱語義的主要內(nèi)容。

3、現(xiàn)代邏輯語義學理論的創(chuàng)始人是美籍波蘭邏輯學家、哲學家A. Tarski，其奠基性文章是他在1933年發(fā)表的形式語言中的真實概念。后來被稱為模型論標準語義學理論。進一步的發(fā)展由維特根斯坦最早提出設想，卡爾納普最早把它展開為系統(tǒng)。這體現(xiàn)在他1947年發(fā)表的 意義和必然性一書中；卡普蘭·克里普克(S.kripke)和蒙太古作出了進一步的貢獻，提出了非經(jīng)典邏輯的語義學理論模態(tài)邏輯語義學(克里普克結(jié)構(gòu))。4.5.2 形式語義基本概念1、 指稱語義：語義是由語義結(jié)構(gòu)和以及在這種結(jié)構(gòu)下公式賦真值的規(guī)定構(gòu)成的。2、 語義結(jié)構(gòu)：對于抽象公理系統(tǒng)或形式系統(tǒng)作出的一種解釋。包括個體域和在這種個體域上的個體

4、運算和個體間關(guān)系。下面給出形式系統(tǒng)語義的定義：3、 形式語義：設FS是已經(jīng)存在的形式系統(tǒng)，F(xiàn)S的語義有語義結(jié)構(gòu)和賦值兩個部分組成：a) 語義結(jié)構(gòu)：當FS的項集TERM不為空時，由非空集合U和規(guī)則組I所組成二元組（U，I），稱為形式系統(tǒng)FS的語義結(jié)構(gòu)。其中U和I的性質(zhì)如下：i. U為非空集合，稱為論域或者個體域；ii. 規(guī)則組I，稱為解釋，根據(jù)規(guī)則組的規(guī)定對項集TERM中的成員指稱到U中的個體；規(guī)定對原子公式如何指稱到U中的個體性質(zhì)（U的子集）、關(guān)系（的子集）。b) 指派：若形式系統(tǒng)FS中的變量集合Variables非空，那么下列映射稱為指派：s：varibles>U。對于給定的語義結(jié)構(gòu)，

5、可以將指派擴展到項集TERM上：TERM>U； S(t) 當t 為變元 S指派t中變元由解釋確定 當t為非變元 F(x,a) = I(f) (x, I(a) = s1( I(f) (x, I(a) = I(f) (s(x), I(a)P(f(a,x) =I(P)(I(f)(a,s(x)c) 賦值：是指一組給公式賦值的規(guī)則，據(jù)此規(guī)則可對每一結(jié)構(gòu)U和指派S確定一由原子公式到值域的映射v：atomic>value。根據(jù)這個賦值規(guī)則，可以將賦值映射進行擴展：v為：d) 可滿足：公式A稱為可滿足，如果存在結(jié)構(gòu)S與指派s，使一個賦值映射v滿足v(A)=1,否則為不可滿足。|=P(f(x,y)F

6、(x,y) s(x,y)=(1,2) s(f(x,y)=I(f)(1,2)=I(f)(s(x),s(y)V(P(x,y)=V(I(P)(s(x),s(y)àV(I(Q)(s(x)4.5.3 一階謂詞語義1、語義結(jié)構(gòu)：一階謂詞形式系統(tǒng)采用TARSKI語義結(jié)構(gòu)。這種語義結(jié)構(gòu)以為其真值集合。每一個Tarski語義結(jié)構(gòu)S，由非空集合U和下列解釋I構(gòu)成：i 常元：對于任一常元a, I(a)U, I(a)記為，為論域中的一個元素；ii 函數(shù)： 對于任一n元函數(shù)為U的一個n元函數(shù)，記為：；iii 謂詞：對于任一n元謂詞，為U上的一個n元關(guān)系，記為，。當n=1時，為U的子集。2、指派：指派S為變元集

7、合到上的映射。S可以擴展為：F(a,x)S(x)=5S(f(a,x)=I(f)(I(a),S(x)= I(f)(I(a),5)i 對于每一變元v：；ii 對于每一常元a：；iii 對于每一個n元函詞fn和項t1，t2.tn：S(F(x1,x2)=F(S(x1),S(x2)由此可見，指派與結(jié)構(gòu)無關(guān)，而與結(jié)構(gòu)相關(guān)。3、賦值：i 賦值映射v：Atomicà定義為：對任何n元謂詞及項t1tn，當且僅當<>，其中。Y>=X+1P(x,y), I(P)=<1,2>,<2,1>,<2,3><3,2> , s(x)=3, s(y)=2

8、?; I(P)(s(x),s(y):P(<3,2>)=1ii 賦值映射v按下列規(guī)則擴展，：l 對原子公式A：；l 對于公式，當且僅當；l 對于公式，當且僅當或；l 對公式，當且僅當對于U中每一元素d， ，其中表示指派S對x指派元素d。4、所有公理為永真式：我們從公理中取公理5來證明，即證明|=為永真式。已知：=1求證：=1任意取一個結(jié)構(gòu)，和這個結(jié)構(gòu)任意一個指派，對于任意一個賦值f，滿足f()=1，則f()=1.任意取一個結(jié)構(gòu),一個賦值映射f，f滿足f()=1：證明：f()=1.f()=1, f()=1,證明:f()=1D, B(d)=1;f(AàB)(d)=1 f(A(d

9、)àB(d)=1; f(A)(d)=1f(A(d)=0,或者f(B(d)=1;f(A)(d)=1 f(B(d)=1對于論域中的任意一個個體，d, f(A(d)àB(d)=1, f(A(d)=1, F(B(d)=1 f( (A(Sx|d)àB(Sx|d) =1 A(d)=1,A(d)àB(d)對于論域中的任意一個個體，d, f(A(Sx|d)1求證：對于論域中的任意一個個體，d, f(B(Sx,|d)1證明：只要證明對任意結(jié)構(gòu)U和指派S，對于任一賦值v：成立。由演繹定理可知，要證明，則只需證明：。因此，只需證明對于任意結(jié)構(gòu)U和指派S，如果U和S滿足：和成立

10、；則在結(jié)構(gòu)U和指派S下在S和U下成立。只需對任意元素d，進行驗證：對于和任意賦值v由于：（1）已知（2）已知由（1）可知，或者或者。由（2）可知，因此。因此，命題成立。5、語義構(gòu)造的例子一階謂詞形式系統(tǒng)的語義結(jié)構(gòu)為：只有一個函詞、一個謂詞和一個常元的形式系統(tǒng)（推理和符號與一階謂詞相同）。P2, f1,a個體域：，即自然數(shù)集合N謂詞：為N上的關(guān)系。函詞：為N上的后繼，即常元：判斷以下公式的真值：=1 v1v2P(v1+1,v2)=1P(x1+1, x1+2)=04.6 一階元理論4.6.1 語法構(gòu)成對于一階謂詞形式系統(tǒng)的語法構(gòu)成，主要有以下定理：ü 獨立性：FSFC的公理集合是獨立的。

11、ü 一致性：FSFC是一致的，即不存在FSFC的公式A，使A及同時成立ü FSFC是不完全的，即存在FSFC的公式A，使A及都不成立。只需證明對于原子公式P(x), P(x), 均不成立。* FSFC的不一致擴充為完全的。A4 -(A->(B->A)ü 半可判定性：FSFC是半可判定的，即存在一個機械的實現(xiàn)過程，能對FSFC中的定理作出肯定判斷，但對非定理的FSFC公式未必能作出否定判決。推廣：設為FSFC的一個可判定公式集（遞歸集），那么的演繹結(jié)果集合是半可判定的。4.6.2 語義結(jié)構(gòu)對于一階謂詞形式系統(tǒng)的語義主要有以下定理：ü 緊致性：對

12、FSFC的任何公式集合，如果的所有有窮子集可滿足，那么也是可滿足的。證明：同命題邏輯。反證法4.6.3 語法語義關(guān)系語法語義關(guān)系，主要有以下定理：ü 合理性：對于FSFC中任一公式A，如果A，那么|=A。合理性推廣：對于FSFC的任一公式集和公式A，若A,則|=A。證明簡單，與命題邏輯基本相同。合理性推論：對于FSFC中任意公式A,B，若AB，則A|=Bü 完備性：對于FSFC的任一公式A，如果|=A，那么A。Godel完備性定理：對于FSFC的任一公式集和公式A，如果|=A，則A。已知：對于任意的結(jié)構(gòu)，和任意的賦值映射f,如果f使得f()=1，則f(A)=1.求證：存在一

13、個證明序列A1,An=A，其中Ai或者為公理，或者為中的元素，或者是由前邊的通過推理規(guī)則得到。證明：對于FSFC的任一公式集是一致的，充要條件為是可滿足的。完備性定理又被稱為Godel完備性定理，其證明思路如下：（1） 對于一階謂詞任意公式集合是一致的，則存在一個一致公式集合，滿足如果公式集合K包含，且K是一致的，則。成為的最大一致擴充。A1,A2,A3=A1,A2,A3,A4=f(A1,A2,A3)=1;f(A)=1;f1(A1,A2,A3,A4,A)=1;F1(A)=1（2）對于的最大一致擴充和公式A，如果A，則有。（3）反證法：假設A ，故有ØØA，從而為一致的。由（

14、1）可知，存在著一極大一致集F，使得ØAF(或者ØAÎF)。根據(jù)前提|=A ，F(xiàn)|=A。由（2）可知F。這與F的一致性矛盾。 5 歸結(jié)原理及應用5.5 標準形式公式標準化的主要目的是對公式進行機械化推理過程。機械化推理過程，是知識工程、邏輯程序設計、人工智能和定理機器證明等理論的基礎(chǔ)。在講述公式標準化過程之前，我們首先介紹整個形式邏輯的基本發(fā)展思路。推理過程： 語義 邏輯推理 反證，真值表合理、完備 公式形式系統(tǒng) 公理，規(guī)則（分離規(guī)則）（機器難以識別）同可滿足 標準形式標準形式 ，代替（機械化）B:B A,A =0假設公式集合S=A1,A2,.,An,假設T=B1

15、,B2,B3,.,Bm這是標準型，這個標準型T和S之間是同可滿足的。如果S是可滿足的，則T是可滿足的。如果T是不可滿足的，則S是不可滿足的。, x=3, B RETE=NETWORK 1965 HPROLOG , 1982 :RULE ENGINE-ILOG目標：反向推理B, B 0:一個集合F>化簡到標準型S，如果集合F是可滿足的，則標準型S是可滿足的。S上出現(xiàn)了0。S是不可滿足。如果S是不可滿足的，則F是不可滿足計算語言Descriptive programming , functional programming language =Rule engine forward PROL

16、OG , LISP 5.5.1 前束范式1、前束范式：稱FSFC的公式為前束范式，當且僅當它有下面的形式：其中Qi,I=1.n是量詞。并且B不含量詞，稱Q1Qn為前束詞，稱B為母式；2、求前束范式a) ；b) ，當x在A中不自由出現(xiàn)；，當x在A中不自由出現(xiàn)；如果有自由出現(xiàn)時，采用改名原理。c) ；à=1,2,10A(1)=A(10)=1或者B(1)=B(10)=1 A(1)vB(1)A(1)vb(1)=A(10)VB(10)=1,或者A(1),A(10)=0或者B(1),B(10)=1A1,3,5,7,9=1, B(2,4,6,8,10)=1A(2,4,6,8,10)=0, B(1,

17、3,5,7,9)=0|=|；ß 1,2,3 A(1)=1;A(2)=0,A(3)=0A(1)=1, B(1)=0;A(2)=0, B(2)=1;A(3)=0=B(3)=0 B(2)=0,B(1)=0,B(3)=0X=1, A(1)&B(1)=0,x=2, A(2)&B(2)=0, x=3, A(3)&B(3)=0àxA(x)&vxB(x)d) ，當x不在B(y)中出現(xiàn)，且y不在A(x)中出現(xiàn);，當x不在B(y)中出現(xiàn)，且y不在A(x)中出現(xiàn);如果有自由出現(xiàn)時，采用改名原理。4、 例：將化成與其等價的前束范式。Ø(Ø (&q

18、uot;x$yF(u,x,y) ($x(Ø"yG(y,w)àH(x)Ø (Ø("x$yF(u,x,y) ($x("yG(y,w)H(x)Ø (Ø("x$yF(u,x,y) ($x"y(G(y,w)H(x)Ø ($xØ$yF(u,x,y)$x"y(G(y,w)H(x)Ø($x"yØF(u,x,y)$x"y(G(y,w)H(x)Ø$x("yØF(u,x,y)"y(G(y,w)H(x

19、)Ø$x("yØF(u,x,y)"y(G(y,w)H(x)"xØ("yØF(u,x,y)"y(G(y,w)H(x)"x (Ø"yØF(u,x,y) Ø"y(G(y,w)H(x)"x ($yF(u,x,y) $yØ (G(y,w)H(x)"x ($yF(u,x,y) $y (Ø G(y,w) Ø H(x)"x ($yF(u,x,y) $z (Ø G(z,w) Ø H(x

20、)"x $y$z (F(u,x,y) Ø G(z,w) Ø H(x)2、定理：對于FSFC中的任一公式，有一個前束范式與其邏輯等價。證.證明實際上是一轉(zhuǎn)換算法：°.聯(lián)結(jié)詞歸約：消去®，«；°.否定詞深入：將否定詞Ø移到到每個原子公式之前;°.約束變項改名：將每個約束變項都改名為互不同名，且與所有的自由變項也不同名;°.量詞"與$前移：將所有的量詞按其在公式中的位置順序全部移到整個公式之前;°.調(diào)整Ù與Ú：將母式化歸為CNF。證明完畢。5.5.2 斯柯倫標準

21、形1 標準化前束范式：基礎(chǔ)，但不夠用。例如： A(a)匹配規(guī)則比較麻煩，而且是機器難于識別的。 B(a) 匹配規(guī)則比較麻煩，而且是機器難于識別的。那么怎樣讓計算機能夠匹配這些公式的關(guān)鍵在于怎樣去掉量詞；對于可以去掉（可滿足性），而則不成。因為：l 與A(c)并不邏輯等價；由；不可能得到，A(c)成立。l (x,f(x) 就更難了；對A(x,c)，要對每一x找到不同的常量c才行。(1,2), (2,f(x),.利用計算機進行邏輯推理的時候，并不需要對公式進行等價轉(zhuǎn)換。只需要和銷去量詞后的公式保持同可滿足性即可。斯柯倫標準型就是為了解決以上的問題。1,2,102、Skolem定理在介紹Skolem

22、定理之前，我們首先看看反證法：證明成立，只需證明為不可滿足的。設與公式集合1. n同可滿足。要證明為不可滿足的，則只需證明I為不可滿足的，其中I為1到n中任意的數(shù)字。I的不可滿足性，就證明了。從而在將公式化為標準形式，不需要之間是等價的，只需時同可滿足的。àQ1àQ2àQ30如果存在一個賦值映射f，使得f()=1,則存在一個賦值映射f1，使得f1(Q1)=1.S1與S2是同可滿足的：指的是如果存在賦值f(S1)=1，則存在賦值f1(S2)=1.A1,A100, A2,A1Skolem定理：對于公式，存在一個不在A中出現(xiàn)的常元c，使得與公式具有同可滿足性；對于公式存

23、在一個不在A中出現(xiàn)的函數(shù)，使得公式與公式具有同可滿足性。其中c稱為斯柯倫常元、稱為Skolem函詞。3、skolem標準形設公式A為前束范式（其母式為析取范式和合取范式）。稱為A的斯柯倫標準形，如果是用skolem常元、skolem函詞消除A中量詞后得到的公式。當A的母式為合取范式時，其斯柯倫標準形稱為合取型，否則稱為析取型。斯柯倫標準型通常的約定為合取型。例：求公式的斯柯倫標準型。求一個公式a的Skolem標準型的算法： °.先將a化為前束范式b1:=Qx1QxnA，其中A為母式，不含量詞。若所有的Qi:="(1£ i £n)，則b1顯然是Skoloe

24、m標準型。取b:=b1 ，即為所求。算法結(jié)束;否則轉(zhuǎn)2° ：2°.若b1形為$x1 "x2"xn A，則選一不在A中出現(xiàn)的個體常項c(稱為Skolem常項),可得 b2:="x2"xn 顯然b2是一Skolem標準型。取b :=b2 ，即為所求。算法結(jié)束; °.若b1形為"x1"xk$xk+1Qk+2xk+2QnxnA，則選一不在A中出現(xiàn)的k元函詞符號f(稱為Skoloem函詞)，可得 b2:="x1"xkQk+2xk+2Qnxn若Qk+2 , Qn全為"，則顯然b2是一Sk

25、olem標準型。取b :=b2 ，即為所求。算法結(jié)束; 否則返回到°自己。完畢。A1=(B1vb2)()()=B1vB2, (), () A, AvB, BA2=B1B2B3B4 =B1,B2,B3,BA1,A2,A3 =A1A2A3 5.5.3 子句集A1,A2,A3= A1&A2&A31、子句集概念對于合取型斯柯倫標準型，其合取項被稱為子句，其析取項被稱為文字。由于每個合取型斯柯倫標準型，有多個子句構(gòu)成。我們可以把一個斯柯倫標準型中的所有子句集合在一起。這樣一個斯柯倫標準型，就有了一個與其對應的等價的子句的集合。公式àSkolem AàC1&C2&C3=C1,C2,C3:C1=L1vL2vL3.公式集合S被稱為公式A的子句集，如果S為A的斯柯倫標準型中全體子句的集合。S稱為可滿足的，如果存在一個結(jié)構(gòu)使S中的每個子句為真；否則稱子句集合為不可滿足的。公式à前束范式àSkolem標準型à子句集例如：子句 文字 (P(x1)vP2(x2), P3(x2)A1A2A3=A1,A2,A32、子句集性質(zhì)l 子句集中兩個子句中變量是獨立的、無關(guān)的，不管子句中的變量名稱是否相同。這主要是因為：。同一子句中的變量是相互依賴的。l 斯柯倫標