一階邏輯等值演算與推理

2023/5/161

第5章一階邏輯等值演算與推理5.1一階邏輯等值式5.2一階邏輯前束范式5.3一階邏輯的推理理論2023/5/1625.1一階邏輯等值式定義5.1設(shè)A,B是一階邏輯中的任意兩公式，若A

B為永真式，稱(chēng)A和B等值，記為AB，稱(chēng)AB

是等值式。基本等值式Group1.命題邏輯中基本等值式的代換實(shí)例

P→Q

┐P

∨Q xP(x)→yE(y)┐xP(x)

∨yE(y) x(P(x)→Q(x))x(┐P

(x)

∨Q(x))

2023/5/1635.1一階邏輯等值式group21.消去量詞等值式對(duì)有限個(gè)體域D＝{a1,a2,…,an}中xA(x)A(a1)∧A(a2)∧……∧A(an)xA(x)A(a1)∨A(a2)∨……∨A(an)2.量詞的否定等值式（全稱(chēng)量詞和存在量詞之間的關(guān)系,A(x)是含x自由出現(xiàn)的公式）┐xA(x)x┐A(x)┐

xA(x)x┐A(x)2023/5/1645.1一階邏輯等值式3.量詞轄域收縮與擴(kuò)張等值式

設(shè)A(x)是含x自由出現(xiàn)的公式，B中不含x的出現(xiàn)關(guān)于全稱(chēng)量詞的：x(A(x)B)xA(x)Bx(A(x)B)xA(x)B

x(A(x)B)xA(x)Bx(BA(x))BxA(x)

關(guān)于存在量詞的:x(A(x)B)xA(x)Bx(A(x)B)xA(x)B

x(A(x)B)xA(x)Bx(BA(x))BxA(x)2023/5/1655.1一階邏輯等值式4.量詞分配等值式設(shè)A(x)和B(x)都是包含自由變?cè)獂的謂詞公式，則：x(A(x)∧B(x))xA(x)∧xB(x)x(A(x)∨B(x))xA(x)∨xB(x)5.量詞的交換xyA(x,y)yxA(x,y)xyA(x,y)yxA(x,y)2023/5/1665.1一階邏輯等值式例5.3：設(shè)個(gè)體域D={a,b,c},消去下面公式中的量詞:(1)x(F(x)G(x))(F(a)G(a))(F(b)G(b))(F(c)G(c))(2)x(F(x)yG(y))xF(x)yG(y)量詞轄域收縮(F(a)F(b)F(c))(G(a)G(b)G(c))x(F(x,a)F(x,b)F(x,c))(3)xyF(x,y)(F(a,a)F(a,b)F(a,c))(F(b,a)F(b,b)F(b,c))(F(c,a)F(c,b)F(c,c))2023/5/1675.1一階邏輯等值式例5.5：證明下列各等值式:

（1）

x(M(x)F(x))x(M(x)F(x))證左邊x(M(x)F(x))量詞否定等值式x(M(x)F(x))x(M(x)F(x))2023/5/1685.1一階邏輯等值式置換規(guī)則、換名規(guī)則、代替規(guī)則1.置換規(guī)則若AB,則(A)

(B).2023/5/1695.1一階邏輯等值式2.換名規(guī)則約束變?cè)膿Q名依據(jù)一個(gè)公式的約束變?cè)墒褂枚鄠€(gè)名稱(chēng)，具體符號(hào)無(wú)關(guān)緊要，故可對(duì)約束變?cè)M(jìn)行換名。例如：xP(x)yP(y)換名規(guī)則將公式A中某量詞的指導(dǎo)變?cè)捌湓谳犛騼?nèi)的所有約束出現(xiàn)改成該量詞轄域內(nèi)未曾出現(xiàn)的某個(gè)個(gè)體變項(xiàng),其余部分不變,記所得公式為A,則AA。2023/5/16105.1一階邏輯等值式例如：xP(x)→Q(x)

yP(y)→Q(x)x(P(x,y)→Q(x,y))∨P(x,z)

t(P(t,y)→Q(t,y))∨P(x,z)2023/5/16115.1一階邏輯等值式3.自由變?cè)拇嬉?guī)則將公式A中某個(gè)自由出現(xiàn)的個(gè)體變項(xiàng)的所有出現(xiàn)用A中未曾使用過(guò)的個(gè)體變項(xiàng)符號(hào)代替，A中其余部分不變，所得公式A’，

則AA。例如：xP(x)→Q(x)xP(x)→Q(y)x(P(x,y)→Q(x,y))∨P(x,z)x(P(x,y)→Q(x,y))∨P(t,z)一階邏輯公式及解釋2023/5/16125.1一階邏輯等值式例5.1

消去公式中既約束出現(xiàn)、又自由出現(xiàn)的個(gè)體變項(xiàng)(1)xF(x,y,z)

yG(x,y,z)uF(u,y,z)

yG(x,y,z)換名規(guī)則uF(u,y,z)

wG(x,w,z)換名規(guī)則或者xF(x,u,z)

yG(x,y,z)代替規(guī)則xF(x,u,z)

yG(v,y,z)代替規(guī)則(2)x(F(x,y)

yG(x,y,z))x(F(x,y)

tG(x,t,z))換名規(guī)則或者x(F(x,t)

yG(x,y,z))代替規(guī)則2023/5/16135.2一階邏輯前束范式定義5.2：設(shè)A為一個(gè)謂詞公式，若A具有如下形式：Q1x1Q2x2……QkxkB（其中：Qi(1≤i≤n)為或，B為不含量詞的公式）則稱(chēng)A為前束范式。例如:xy(F(x)(G(y)H(x,y)))

x(F(x)G(x))

x(F(x)y(G(y)H(x,y))) x(F(x)G(x)) 2023/5/16145.2一階邏輯前束范式例5.6(P71)

：求如下公式的前束范式：xF(x)∧┐xG(x)xF(x)∨┐xG(x)定理5.1：(前束范式存在定理)一階邏輯中的任何公式都存在與之等值的前束范式。例5.7(P73)

2023/5/16155.3一階邏輯的推理理論1.推理的形式結(jié)構(gòu)形式1：A1A2…AkB形式2：前提：A1,A2,…,Ak

結(jié)論：B若A1A2…AkB為永真式,則稱(chēng)推理正確,記作A1A2…AkB證明方法：構(gòu)造證明法：一階邏輯的推理理論2023/5/16165.3一階邏輯的推理理論一階邏輯自然推理系統(tǒng)N

定義5.3：自然推理系統(tǒng)N定義如下：字母表合式公式推理規(guī)則命題邏輯的推理規(guī)則一階邏輯的推理定律2023/5/16175.3一階邏輯的推理理論一階邏輯的推理定律Group1:命題邏輯推理定律的代換實(shí)例；命題演算中的永真蘊(yùn)涵式，以及由代入規(guī)則生成的永真蘊(yùn)涵式； （P→Q）∧P

Q

（xP(x)

→yE(y)）∧

xP(x)yE(y)Group2:由基本等值式生成的推理定律一階邏輯推理理論2023/5/16185.3一階邏輯的推理理論Group3:一階邏輯的兩個(gè)重言蘊(yùn)含式（1）

xA(x)∨xB(x)x(A(x)∨B(x))證明：若xA(x)∨xB(x)為1，即xA(x)為1，或xB(x)為1，故x(A(x)∨B(x))為1。找反例說(shuō)明二者不等值D

：正整數(shù)集合A(x) ：x是奇數(shù)B(x) ：x是偶數(shù)一階邏輯等值式和前束范式2023/5/16195.3一階邏輯的推理理論Group3:一階邏輯的兩個(gè)重言蘊(yùn)含式（2）x(A(x)∧B(x))xA(x)∧xB(x)證明：若x(A(x)∧B(x))為1，即至少有一個(gè)c∈D，使A(c)∧

B(c)為1，也就是A(c)為1，B(c)為1，故xA(x)∧xB(x)為1。找反例說(shuō)明二者不等值

D：正整數(shù)集合

A(x)：x是奇數(shù)；

B(x)：x是偶數(shù)一階邏輯等值式和前束范式2023/5/16205.3一階邏輯的推理理論Group4:量詞的消去與引入規(guī)則1.全稱(chēng)量詞消去規(guī)則(UniversalIdentification，-)c是論域中的任意個(gè)體。2023/5/16215.3一階邏輯的推理理論Group4:量詞的消去與引入規(guī)則2.全稱(chēng)量詞引入規(guī)則(UniversalGeneralization，+)c是論域中的任意個(gè)體。2023/5/16225.3一階邏輯的推理理論Group4:量詞的消去與引入規(guī)則

3.存在量詞引入規(guī)則(ExistentialGeneralization，+)c是論域中的某個(gè)個(gè)體。2023/5/16235.3一階邏輯的推理理論c是論域中的某個(gè)個(gè)體。Group4:量詞的消去與引入規(guī)則

4.存在量詞消去規(guī)則(ExistentialIdentification，-)2023/5/16245.3一階邏輯的推理理論例:證明蘇格拉底論證是有效的。證明：設(shè)F(x):x是人，G(x):x是要死的，a：蘇格拉底則格拉底論證符號(hào)化為：前提：x(F(x)→G(x))，F(xiàn)(a)

結(jié)論：G(a)x(F(x)→G(x)) 前提引入F(a)→G(a) ①-

F(a) 前提引入G(a) ②,③