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

1、形式系統(tǒng)形式系統(tǒng)由, term, formula, axiom, rule等5個(gè)部分構(gòu)成，其中 稱為符號(hào)表，term為項(xiàng)集；forumula為公式集；aixiom為公理集；rule為推理規(guī)則集。：1、 符號(hào)表為非空集合，其元素稱為符號(hào)。2、 設(shè)為上全體字的組合構(gòu)成的集合。項(xiàng)集term為的子集，其元素稱為項(xiàng)；項(xiàng)集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ī)則。其中公式集和項(xiàng)集之間沒有交叉，即termformula =，公式和項(xiàng)統(tǒng)稱為表達(dá)式。由定義可知，符號(hào)表、項(xiàng)集term、公式集formula是形式系統(tǒng)的語言部分。而公理集axiom、推理規(guī)則集rule為推理部分形式系統(tǒng)特性1、 符號(hào)表為非空、可數(shù)集合（有窮、無窮都可以）。2、 項(xiàng)集term、公式集formula、公理集axiom和推理規(guī)則集rule是遞歸集合，即必須存在一個(gè)算法能夠判定給定符號(hào)串是否屬于集合（可判定的）。3、 形式系統(tǒng)中的項(xiàng)是用來描述研究的對(duì)象，

3、或者稱為客觀世界的。而公式是用來描述這些研究對(duì)象的性質(zhì)的。這個(gè)語言被稱為對(duì)象語言。定義公式和項(xiàng)產(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是一個(gè)有關(guān)公式的性質(zhì)證明：r對(duì)于所有公式有效i. 對(duì)于，則ii. 假設(shè)公式a和b都具有riii. ，且，則iv. 是公式，如果且，則根據(jù)：形式系統(tǒng)的聯(lián)結(jié)詞只有兩個(gè)，因?yàn)樵诿}邏輯的語義上，其他聯(lián)結(jié)詞可以有這兩個(gè)聯(lián)結(jié)詞表示。已知：求證：a成立(1)a是公式(2)，反證(3) 3公理代入原理：設(shè)a(p)為含有變?cè)猵的公理（定理同樣適用），如果將公式a中的變?cè)猵替換為命題變?cè)猙，則a(b)仍為公理（定理）；（公理填充）等價(jià)替換原理：設(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.由此，命題成立。給出一個(gè)形式系統(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è)主要部分構(gòu)成）*確定研究對(duì)象集合，論域

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

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

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

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

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

12、推理規(guī)則得到。因此，a1是公理，也就是a是公理。對(duì)于任意的賦值映射f，則f(a)=1。假設(shè)：n<m時(shí)，命題成立：a是定理則a是永真的。證明：當(dāng)n=m時(shí)，命題成立。a1,a2,am-1, am=a v1, am是公理：公理是永真的，因此命題成立。2, am是前邊通過推理規(guī)則得到的。推理分離規(guī)則，三段論。假設(shè)am是由ai和aj通過分離規(guī)則得到。由于歸納假設(shè)，ai和aj都是永真的。由于推理規(guī)則保真性，那么am是永真的。因此，命題成立。自由變?cè)鹤杂勺冊(cè)钦嬲淖冊(cè)?，可以將個(gè)體域中的任意個(gè)體代入到自由變?cè)?。類似于?shù)學(xué)中的變?cè)?。約束變?cè)杭s束變?cè)⒉皇菍?shí)際意義的變?cè)〝?shù)學(xué)意義上的變?cè)?。約束變?cè)?/p>

13、是為表達(dá)某種想的輔助符號(hào)。自由變?cè)s束變?cè)纱氩豢纱氩豢筛拿筛拿吭~中的變?cè)蔀橹笇?dǎo)變?cè)?，指?dǎo) 4變?cè)羌s束變?cè)拿恚涸趂sfc中，稱公式a´為公式a的改名式，如果將a中至少一個(gè)量詞的指導(dǎo)變?cè)拖鄳?yīng)的約束變?cè)ㄈ绻校┒几臑榱硪粋€(gè)相同名字的變?cè)蟮玫降墓絘。在fsfc中，如果a為公式a的改命式，且a改用的變?cè)赼中無任何出現(xiàn)，那么aa。量詞規(guī)則全稱（）消去規(guī)則：如果，且項(xiàng)t對(duì)于公式為可代入的，則。全稱（）引入規(guī)則：如果，t不在中出現(xiàn)，則。存在（）銷去規(guī)則：設(shè)為fsfc的任意公式集合，a, b為公式。變?cè)獂在和公式b中無出現(xiàn)。如果，則b。存在（）引入規(guī)則：設(shè)為fsfc的任意

14、公式集合，b為公式。變?cè)獂在和公式b中無出現(xiàn)。如果b，則。形式語義基本概念1、 指稱語義：語義是由語義結(jié)構(gòu)和以及在這種結(jié)構(gòu)下公式賦真值的規(guī)定構(gòu)成的。2、 語義結(jié)構(gòu)：對(duì)于抽象公理系統(tǒng)或形式系統(tǒng)作出的一種解釋。包括個(gè)體域和在這種個(gè)體域上的個(gè)體運(yùn)算和個(gè)體間關(guān)系。下面給出形式系統(tǒng)語義的定義：3、 形式語義：設(shè)fs是已經(jīng)存在的形式系統(tǒng)，fs的語義有語義結(jié)構(gòu)和賦值兩個(gè)部分組成：a) 語義結(jié)構(gòu)：當(dāng)fs的項(xiàng)集term不為空時(shí)，由非空集合u和規(guī)則組i所組成二元組（u，i），稱為形式系統(tǒng)fs的語義結(jié)構(gòu)。其中u和i的性質(zhì)如下：i. u為非空集合，稱為論域或者個(gè)體域；ii. 規(guī)則組i，稱為解釋，根據(jù)規(guī)則組的規(guī)定對(duì)項(xiàng)集

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

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

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

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

19、定為合取型。例：求公式的斯柯倫標(biāo)準(zhǔn)型。求一個(gè)公式a的skolem標(biāo)準(zhǔn)型的算法： °.先將a化為前束范式b1:=qx1qxna，其中a為母式，不含量詞。若所有的qi:="(1£ i £n)，則b1顯然是skoloem標(biāo)準(zhǔn)型。取b:=b1 ，即為所求。算法結(jié)束;否則轉(zhuǎn)2° ：2°.若b1形為$x1 "x2"xn a，則選一不在a中出現(xiàn)的個(gè)體常項(xiàng)c(稱為skolem常項(xiàng)),可得 b2:="x2"xn 顯然b2是一skolem標(biāo)準(zhǔn)型。取b :=b2 ，即為所求。算法結(jié)束; °.若b1形為&qu

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

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

22、集的子集都是可滿足的。相反，如果一個(gè)子句集的子集是不可滿足的，則子句集是不可滿足的。求子句集通常通過以下步驟，可以得到一個(gè)公式的子句集。1.求a的合取型前束范式2.求a的skolem標(biāo)準(zhǔn)形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標(biāo)準(zhǔn)型 子句集子句1子句2二元?dú)w結(jié)：為分別為fspc中，含有互補(bǔ)文字的子句，l1= l2那么下面推理稱為二元?dú)w結(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代換需要注意的是：首先代換不能是自身代換，用同一變量代換本身是沒有什么意義的；其次，對(duì)于代換的過程是一次性將所有的變量同時(shí)代換成項(xiàng)，而不是先代換第一項(xiàng)，再代換第二項(xiàng)的順序結(jié)構(gòu)。設(shè)公式為，代換為，求代換