北郵高級數(shù)理邏輯課件

1、形式系統(tǒng)形式系統(tǒng)由, term, formula, axiom, rule等5個部分構(gòu)成，其中 稱為符號表，term為項集；forumula為公式集；aixiom為公理集；rule為推理規(guī)則集。：1、 符號表為非空集合，其元素稱為符號。2、 設(shè)為上全體字的組合構(gòu)成的集合。項集term為的子集，其元素稱為項；項集term有子集variable稱為變量集合，其元素稱為變量。f(x) a, x, 3、 設(shè)為上全體字的組合構(gòu)成的集合。公式結(jié)formula為的子集，其元素稱為公式；公式集有子集atom，其元素稱為原子公式。 a(f(a,x1,y), aàb4、 公理集axiom是公式集from

2、ula的子集，其元素稱為公理。5、 推理規(guī)則集rule是公式集formula上的n元關(guān)系集合，即rule=，其元素稱為形式系統(tǒng)的推理規(guī)則。其中公式集和項集之間沒有交叉，即termformula =，公式和項統(tǒng)稱為表達式。由定義可知，符號表、項集term、公式集formula是形式系統(tǒng)的語言部分。而公理集axiom、推理規(guī)則集rule為推理部分形式系統(tǒng)特性1、 符號表為非空、可數(shù)集合（有窮、無窮都可以）。2、 項集term、公式集formula、公理集axiom和推理規(guī)則集rule是遞歸集合，即必須存在一個算法能夠判定給定符號串是否屬于集合（可判定的）。3、 形式系統(tǒng)中的項是用來描述研究的對象，

3、或者稱為客觀世界的。而公式是用來描述這些研究對象的性質(zhì)的。這個語言被稱為對象語言。定義公式和項產(chǎn)生方法的規(guī)則稱為詞法。公理：iiiiii證明：aàa(1)aà(aàa)(aà(bàc)à(aàb)à(aàc)(aà(bàa)à(aàb)à(aàa)(aà(aàa)àa)à(aà(aàa)à(aàa)aà(aàa)àa)(aà(a

4、àa)à(aàa)(aà(aàa)aàa分離規(guī)則已知：r是一個有關(guān)公式的性質(zhì)證明：r對于所有公式有效i. 對于，則ii. 假設(shè)公式a和b都具有riii. ，且，則iv. 是公式，如果且，則根據(jù)：形式系統(tǒng)的聯(lián)結(jié)詞只有兩個，因為在命題邏輯的語義上，其他聯(lián)結(jié)詞可以有這兩個聯(lián)結(jié)詞表示。已知：求證：a成立(1)a是公式(2)，反證(3) 3公理代入原理：設(shè)a(p)為含有變元p的公理（定理同樣適用），如果將公式a中的變元p替換為命題變元b，則a(b)仍為公理（定理）；（公理填充）等價替換原理：設(shè)命題公式a含有子公式c（c為命題公式），如果cd，那

5、么將a中子公式c提換為命題公式d（不一定全部），所得公式b滿足ab。緊致性：設(shè)為fspc上的公式集合，a為fspc的公式。如果，則存在的有限子集0 使得0 。已知：aà(bàc), b證明：aàc公理推演：aà(bàc)abàc bc自然推演：f(b)=1,f(a)=0或者f(bàc)=1。假設(shè)f(a)=0;則f(aàc)=1.假設(shè)f(a)=1,那么f(bàc)=1.f(b)=1,則f(c)=1.因此，f(aàc)=1.由此，命題成立。給出一個形式系統(tǒng)，其公理定義如下：a, (,), à

6、;,-給出公理如下：aàaaàaàa(aàa)à(aàa)(aàa)à(aàa)(a->a->a)->(a->a)下列哪些是定理？aàaà(aàa)(aàa)à(aàa)à(aàa)(aàaàa)à(aàaàa)(aàb)à(aàb)à(aàb)語義構(gòu)成結(jié)構(gòu)：（有兩個主要部分構(gòu)成）*確定研究對象集合，論域

7、或個體域*把形式系統(tǒng)中的變量到論域中的一組規(guī)則映射規(guī)則域值：指一組給公式賦值的規(guī)則根據(jù)這項規(guī)則將 atomicvalue中語義的特殊公式1) 公式a為永真式，重言式tautologies，如果對一切賦值，.2) 公式a為永假式，矛盾式contradictions,如果對一切賦值，3) a，b為邏輯等價的，如果對于一切賦值，記做ab(a|=|b)4) 公式a為可滿足的，如果至少存在一個賦值，邏輯推論：設(shè)是一個fspc上的公式集合，a是fspc上的任一公式。a為的邏輯結(jié)果，記做|=a，當且僅當對任何賦值映射v，如果1時，則。|=讀作邏輯蘊涵。邏輯等價：設(shè)公式a和公式b分別為fspc上的兩個公式。a

8、和b為邏輯等價的，記做a|=|b當且僅當a|=b和b|=a同時成立。永真式：如果a為永真式，則公式集合為空集，即|=a。演繹定理：設(shè)為fspc的公式集合，a和b分別為fspc上的公式。|=成立的充分必要條件是：|=。證明：從語義上：必要性：由于f1()=1，則f1(aàb)=1;由于f1(aàb)=1,并且f1(a)=1，則f(b)=1充分性：對于映射f，若f()=1，假設(shè)f1(a)=0;f1(aàb)=1.假設(shè)f1(a)=1, 由于已知條件可以知道f(b)=1.因此，f(aàb)=1從形式上：必要性：1成立，則成立。對于成立有兩種情況，為了證明成立，只

9、需考慮，使1的情況。如果賦值映射v，滿足1，1且，則有1。因此，成立。充分性：任取賦值映射v，滿足，則有：當0時，有當1時，由已知1， 因此聯(lián)結(jié)詞的完備集：聯(lián)結(jié)詞的集合為完備的，當且僅當對于其他的聯(lián)結(jié)詞都可以由這個聯(lián)結(jié)詞的集合中的元素來表示。fspc中的完備集：、等。如果引入異或，那么異或與也構(gòu)成一個完備集合。形式化系統(tǒng)à語義結(jié)構(gòu)à元理論à自動化語法構(gòu)成語法構(gòu)成研究形式系統(tǒng)語言構(gòu)成規(guī)律。主要研究推演（重寫）規(guī)律；主要規(guī)律：（1）獨立性：如果形式系統(tǒng)中每一個公理都是獨立的，即把任一公里a從形式系統(tǒng)中刪除后，所得形式系統(tǒng)fs不滿足fsa（即a不是fs的定理），則稱形式

10、系統(tǒng)為獨立的；l 獨立形式系統(tǒng)是簡潔的；（2）一致性：形式系統(tǒng)fs稱為一致性，或相容的（consistent）如果不存在fs的公式a，使得a，同時成立；l 所有形式系統(tǒng)都應(yīng)該是一致的；（3）完全性：形式系統(tǒng)為完全的，如果對形式系統(tǒng)中任意公式a，或者a成立，或者成立；l 完全性的形式系統(tǒng)，一切都是可知的；因此，幾乎沒有價值；（4）可判定性：形式系統(tǒng)fs稱為可判定的，如果存在一個算法，對fs對的任一公式a，可確定a是否成立，否則稱fs是可判定的；如果上述算法對定理能作出判斷，而對于非定理未必終止（作判斷），稱fs為半可判定的；l fs為可判定的，當且僅當定理集合為遞歸集；（5）公式集合一致性：稱形

11、式系統(tǒng)的公式集合為一致的，如果形式系統(tǒng)是一致的，且不存在公式a使，a ， 同時成立。語法和語義關(guān)系合理性（soundness）：稱形式系統(tǒng)fs是合理的，fs的任意公式a有：fs，則|=m，m為所有結(jié)構(gòu)；完備性（completeness）：稱形式系統(tǒng)fs是完備的，如果對fs的任意公式有：若|=m，則fs，這里m為fs所討論的一類結(jié)構(gòu)；緊致性：稱形式系fs是緊致的，如果對fs的任意公式集有：如果公式集的所有窮子集是可滿足的，那么公式集也是可滿足的；合理性證明：已知：a是定理求證：a是永真的由于a是定理，存在一個證明序列a1,a2,an=a。n=1時：a1=a。由于a1或者為公理或者是前邊的公式通過

12、推理規(guī)則得到。因此，a1是公理，也就是a是公理。對于任意的賦值映射f，則f(a)=1。假設(shè)：n<m時，命題成立：a是定理則a是永真的。證明：當n=m時，命題成立。a1,a2,am-1, am=a v1, am是公理：公理是永真的，因此命題成立。2, am是前邊通過推理規(guī)則得到的。推理分離規(guī)則，三段論。假設(shè)am是由ai和aj通過分離規(guī)則得到。由于歸納假設(shè)，ai和aj都是永真的。由于推理規(guī)則保真性，那么am是永真的。因此，命題成立。自由變元：自由變元是真正的變元，可以將個體域中的任意個體代入到自由變元中。類似于數(shù)學(xué)中的變元。約束變元：約束變元并不是實際意義的變元（數(shù)學(xué)意義上的變元）。約束變元

13、是為表達某種想的輔助符號。自由變元約束變元可代入不可代入不可改名可改名量詞中的變元成為指導(dǎo)變元，指導(dǎo) 4變元是約束變元改名原理：在fsfc中，稱公式a´為公式a的改名式，如果將a中至少一個量詞的指導(dǎo)變元和相應(yīng)的約束變元（如果有）都改為另一個相同名字的變元后得到的公式a。在fsfc中，如果a為公式a的改命式，且a改用的變元在a中無任何出現(xiàn)，那么aa。量詞規(guī)則全稱（）消去規(guī)則：如果，且項t對于公式為可代入的，則。全稱（）引入規(guī)則：如果，t不在中出現(xiàn)，則。存在（）銷去規(guī)則：設(shè)為fsfc的任意公式集合，a, b為公式。變元x在和公式b中無出現(xiàn)。如果，則b。存在（）引入規(guī)則：設(shè)為fsfc的任意

14、公式集合，b為公式。變元x在和公式b中無出現(xiàn)。如果b，則。形式語義基本概念1、 指稱語義：語義是由語義結(jié)構(gòu)和以及在這種結(jié)構(gòu)下公式賦真值的規(guī)定構(gòu)成的。2、 語義結(jié)構(gòu)：對于抽象公理系統(tǒng)或形式系統(tǒng)作出的一種解釋。包括個體域和在這種個體域上的個體運算和個體間關(guān)系。下面給出形式系統(tǒng)語義的定義：3、 形式語義：設(shè)fs是已經(jīng)存在的形式系統(tǒng)，fs的語義有語義結(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ī)定對項集

15、term中的成員指稱到u中的個體；規(guī)定對原子公式如何指稱到u中的個體性質(zhì)（u的子集）、關(guān)系（的子集）。b) 指派：若形式系統(tǒng)fs中的變量集合variables非空，那么下列映射稱為指派：s：varibles>u。對于給定的語義結(jié)構(gòu)，可以將指派擴展到項集term上：term>u； s(t) 當t 為變元 s指派t中變元由解釋確定 當t為非變元c) 賦值：是指一組給公式賦值的規(guī)則，據(jù)此規(guī)則可對每一結(jié)構(gòu)u和指派s確定一由原子公式到值域的映射v：atomic>value。根據(jù)這個賦值規(guī)則，可以將賦值映射進行擴展：v為：d) 可滿足：公式a稱為可滿足，如果存在結(jié)構(gòu)s與指派s，使一個賦值

16、映射v滿足v(a)=1,否則為不可滿足。一階謂詞語義1、語義結(jié)構(gòu)：一階謂詞形式系統(tǒng)采用tarski語義結(jié)構(gòu)。這種語義結(jié)構(gòu)以為其真值集合。每一個tarski語義結(jié)構(gòu)s，由非空集合u和下列解釋i構(gòu)成：1. 常元：對于任一常元a, i(a)u, i(a)記為，為論域中的一個元素；2. 函數(shù)： 對于任一n元函數(shù)為u的一個n元函數(shù)，記為：；3. 謂詞：對于任一n元謂詞，為u上的一個n元關(guān)系，記為，。當n=1時，為u的子集。2、指派：指派s為變元集合到上的映射。s可以擴展為：對于每一變元v：；對于每一常元a：；對于每一個n元函詞fn和項t1，t2.tn：由此可見，指派與結(jié)構(gòu)無關(guān)，而與結(jié)構(gòu)相關(guān)。3、賦值：i

17、 賦值映射v：atomicà定義為：對任何n元謂詞及項t1tn，當且僅當<>，其中。ii 賦值映射v按下列規(guī)則擴展，：對原子公式a：；對于公式，當且僅當；對于公式，當且僅當或；對公式，當且僅當對于u中每一元素d， ，其中表示指派s對x指派元素d。已知：任意取一個結(jié)構(gòu),一個賦值映射f，f滿足f()=1：證明：f()=1.設(shè)x取值為df(aàb)(d)=1 f(a(d)àb(d)=1; f(a)(d)=1f(b(d)=1對于論域中的任意一個個體，d, f(a(d)àb(d)=1, f(a(d)=1, f(b(d)=1一階謂詞形式系統(tǒng)的語義結(jié)構(gòu)：只

18、有一個函詞、一個謂詞和一個常元的形式系統(tǒng)（推理和符號與一階謂詞相同）。個體域：，即自然數(shù)集合n謂詞：為n上的關(guān)系。函詞：為n上的后繼，即常元：判斷以下公式的真值：=1=1=0形式邏輯基本發(fā)展思路推理過程： 語義邏輯推理 反證，真值表合理、完備 公式形式系統(tǒng) 公理，規(guī)則（分離規(guī)則）（機器難以識別）同可滿足 標準形式標準形式 ，代替（機械化）為什么同可滿足？skolem標準形設(shè)公式a為前束范式（其母式為析取范式和合取范式）。稱為a的斯柯倫標準形，如果是用skolem常元、skolem函詞消除a中量詞后得到的公式。當a的母式為合取范式時，其斯柯倫標準形稱為合取型，否則稱為析取型。斯柯倫標準型通常的約

19、定為合取型。例：求公式的斯柯倫標準型。求一個公式a的skolem標準型的算法： °.先將a化為前束范式b1:=qx1qxna，其中a為母式，不含量詞。若所有的qi:="(1£ i £n)，則b1顯然是skoloem標準型。取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形為&qu

20、ot;x1"xk$xk+1qk+2xk+2qnxna，則選一不在a中出現(xiàn)的k元函詞符號f(稱為skoloem函詞)，可得 b2:="x1"xkqk+2xk+2qnxn若qk+2 , qn全為"，則顯然b2是一skolem標準型。取b :=b2 ，即為所求。算法結(jié)束; 否則返回到°自己。子句集概念對于合取型斯柯倫標準型，其合取項被稱為子句，其析取項被稱為文字。由于每個合取型斯柯倫標準型，有多個子句構(gòu)成。我們可以把一個斯柯倫標準型中的所有子句集合在一起。這樣一個斯柯倫標準型，就有了一個與其對應(yīng)的等價的子句的集合。公式àskolem a&#

21、224;c1&c2&c3=c1,c2,c3:c1=l1vl2vl3.公式集合s被稱為公式a的子句集，如果s為a的斯柯倫標準型中全體子句的集合。s稱為可滿足的，如果存在一個結(jié)構(gòu)使s中的每個子句為真；否則稱子句集合為不可滿足的。公式à前束范式àskolem標準型à子句集子句集性質(zhì)（1） 子句集中兩個子句中變量是獨立的、無關(guān)的，不管子句中的變量名稱是否相同。這主要是因為：。同一子句中的變量是相互依賴的。（2） 斯柯倫標準型與源公式之間是同可滿足的，斯柯倫標準型與子句集之間是等價的。因此，子句集與原公式之間是同可滿足的。（3） 如果子句集是可滿足的，則子句

22、集的子集都是可滿足的。相反，如果一個子句集的子集是不可滿足的，則子句集是不可滿足的。求子句集通常通過以下步驟，可以得到一個公式的子句集。1.求a的合取型前束范式2.求a的skolem標準形3.求skolem的析取范式4.將skolem析取范式改為子句例：求公式的子句集。"x$y($z(p(x,y) q(x,z) $zr(x,y,z)"x$y$z(p(x,y) q(x,z) r(x,y,z)"x$y$z(r(x,y,z) p(x,y) (q(x,z) r(x,y,z)"x$z(r(x,f1(x),z) p(x,f1(x) (q(x,z) r(x,f1(x)

23、,z)"x(r(x,f1(x),f2(x) p(x,f1(x) (q(x,f2(x) r(x,f1(x),f2(x)(r(x,f1(x),f2(x) p(x,f1(x) (q(x,f2(x) r(x,f1(x),f2(x)子句集為：r(x,f1(x),f2(x) p(x,f1(x)， q(x,f2(x) r(x,f1(x),f2(x) 前束范式 合取范式 skolem標準型 子句集子句1子句2二元歸結(jié)：為分別為fspc中，含有互補文字的子句，l1= l2那么下面推理稱為二元歸結(jié)：c1 , c2 其中，稱c1 , c2為歸結(jié)母式，為歸結(jié)結(jié)果，l1l2為歸結(jié)基。已知：c為c1和c2的歸結(jié)

24、結(jié)果，求證：c為的邏輯結(jié)果。c=c1=(c1-l1)vl1c2=(c2-l2)vl2f(c1)=1，f(c2)=1 f(l1)=1,則f(l2)=0f(l1)=0,則f(l2)=1f(c)=f(c1-l1)v f(c2-l2)c1=(c1-l1)vl1f(l1)=0, f(c1-l1)=1 因此，f(c)=1f(l1)=1，f(l2)=0，則f(c2-l2)=1，f(c2)=f(c2-l2)vf(l2)f(c)=1代換需要注意的是：首先代換不能是自身代換，用同一變量代換本身是沒有什么意義的；其次，對于代換的過程是一次性將所有的變量同時代換成項，而不是先代換第一項，再代換第二項的順序結(jié)構(gòu)。設(shè)公式為，代換為，求代換