1、1主要內容主要內容l 一階邏輯等值式與基本的等值式一階邏輯等值式與基本的等值式l 置換規則、換名規則、代替規則置換規則、換名規則、代替規則l 前束范式前束范式l 自然推理系統自然推理系統NL 及其推理規則及其推理規則第五章第五章 一階邏輯等值演算與推理一階邏輯等值演算與推理25.1 一階邏輯等值式與置換規則一階邏輯等值式與置換規則定義定義5.1 設設A, B是兩個謂詞公式是兩個謂詞公式, 如果如果AB是永真式是永真式, 則稱則稱A與與B等值等值, 記作記作AB, 并稱并稱AB是是等值式等值式基本等值式基本等值式第一組第一組 命題邏輯中命題邏輯中16組基本等值式的代換實例組基本等值式的代換實例

2、例如，例如，xF(x)xF(x), xF(x)yG(y) xF(x)yG(y) 等等第二組第二組 (1) 消去量詞等值式消去量詞等值式 設設D =a1, a2, , an xA(x) A(a1) A(a2) A(an) xA(x) A(a1) A(a2) A(an)3基本等值式基本等值式(2) 量詞否定等值式量詞否定等值式 xA(x) x A(x) xA(x) x A(x)(3) 量詞轄域收縮與擴張等值式量詞轄域收縮與擴張等值式. A(x) 是含是含 x 自由出現的公式，自由出現的公式，B 中不含中不含 x 的自由出現的自由出現 關于全稱量詞的：關于全稱量詞的： x(A(x) B) xA(x)

3、 B x(A(x) B) xA(x) B x(A(x)B) xA(x)B x(BA(x) BxA(x) 4基本等值式基本等值式 關于存在量詞的：關于存在量詞的： x(A(x) B) xA(x) B x(A(x) B) xA(x) B x(A(x)B) xA(x)B x(BA(x) BxA(x)(4) 量詞分配等值式量詞分配等值式 x(A(x) B(x) xA(x)xB(x) x(A(x) B(x) xA(x)xB(x)注意：注意： 對對 ， 對對 無分配律無分配律A(x) : x是奇數B(x) : x是偶數5置換規則、換名規則、代替規則置換規則、換名規則、代替規則1. 置換規則置換規則 設設

4、(A)是含是含A的公式的公式, 那么那么, 若若AB, 則則 (A) (B).2. 換名規則換名規則 設設A為一公式，將為一公式，將A中某量詞轄域中個體變項的所有約束中某量詞轄域中個體變項的所有約束 出現及相應的指導變元換成該量詞轄域中未曾出現過的個出現及相應的指導變元換成該量詞轄域中未曾出現過的個 體變項符號，其余部分不變，設所得公式為體變項符號，其余部分不變，設所得公式為A ，則，則AA.3. 代替規則代替規則 設設A為一公式，將為一公式，將A中某個個體變項的所有自由出現用中某個個體變項的所有自由出現用A中中 未曾出現過的個體變項符號代替，其余部分不變，設所得未曾出現過的個體變項符號代替，

5、其余部分不變，設所得 公式為公式為A ，則，則AA.6實例實例例例1 將下面命題用兩種形式符號化將下面命題用兩種形式符號化, 并證明兩者等值并證明兩者等值: (1) 沒有不犯錯誤的人沒有不犯錯誤的人解解 令令F(x)：x是人，是人，G(x)：x犯錯誤犯錯誤. x(F(x)G(x) 或或 x(F(x)G(x) x(F(x)G(x) x (F(x) G(x) 量詞否定等值式量詞否定等值式 x( F(x) G(x) 置換置換 x(F(x)G(x) 置換置換7實例實例(2) 不是所有的人都愛看電影不是所有的人都愛看電影解解 令令F(x)：x是人，是人，G(x)：愛看電影：愛看電影. x(F(x)G(x

6、) 或或 x(F(x)G(x) x(F(x)G(x) x (F(x)G(x) 量詞否定等值式量詞否定等值式 x ( F(x) G(x) 置換置換 x(F(x)G(x) 置換置換8實例實例例例2 將公式化成等值的不含既有約束出現、又有自由出現將公式化成等值的不含既有約束出現、又有自由出現的個體變項的個體變項: x(F(x,y,z)yG(x,y,z)解解 x(F(x,y,z)yG(x,y,z) x(F(x,y,z)tG(x,t,z) 換名規則換名規則 x t(F(x,y,z)G(x,t,z) 轄域擴張等值式轄域擴張等值式或者或者 x(F(x,y,z)yG(x,y,z) x(F(x,u,z)yG(x

7、,y,z) 代替規則代替規則 x y(F(x,u,z)G(x,y,z) 轄域擴張等值式轄域擴張等值式9實例實例例例3 設個體域設個體域D=a,b,c, 消去下述公式中的量詞消去下述公式中的量詞: (1) x y(F(x)G(y)解解 x y(F(x)G(y) ( y(F(a)G(y) ( y(F(b)G(y) ( y(F(c)G(y) (F(a)G(a) (F(a)G(b) (F(a)G(c) (F(b)G(a) (F(b)G(b) (F(b)G(c) (F(c)G(a) (F(c)G(b) (F(c)G(c) 10實例實例解法二解法二 x y(F(x)G(y) x(F(x)yG(y) 轄域縮

8、小等值式轄域縮小等值式 x(F(x)G(a) G(b) G(c) (F(a)G(a) G(b) G(c) (F(b)G(a) G(b) G(c) (F(c)G(a) G(b) G(c)11實例實例(2) x yF(x,y) x yF(x,y) x(F(x,a) F(x,b) F(x,c) (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)125.2 一階邏輯前束范式一階邏輯前束范式定義定義5.2 設設A為一個一階邏輯公式，若為一個一階邏輯公式，若A具有如下形式具有如下形式 Q1x1Q2x2QkxkB則稱則稱A為為前

9、束范式前束范式，其中，其中Qi (1 i k)為為 或或 ，B為不含量詞為不含量詞的公式的公式. 例如，例如， x (F(x) G(x) x y(F(x)(G(y) H(x,y) 是前束范式是前束范式而而 x(F(x) G(x) x(F(x)y(G(y) H(x,y) 不是前束范式，不是前束范式， 13前束范式存在定理前束范式存在定理定理定理5.1（前束范式存在定理）（前束范式存在定理） 一階邏輯中的任何公式都存在與之等值的前束范式一階邏輯中的任何公式都存在與之等值的前束范式例例4 求下列公式的前束范式求下列公式的前束范式 (1) x(M(x) F(x)解解 x(M(x) F(x) x( M(

10、x)F(x) （量詞否定等值式）（量詞否定等值式） x(M(x)F(x) 后兩步結果都是前束范式，說明公式的前束范式不惟一后兩步結果都是前束范式，說明公式的前束范式不惟一.14求前束范式的實例求前束范式的實例 (2) xF(x)xG(x)解解 xF(x)xG(x) xF(x)x G(x) （量詞否定等值式）（量詞否定等值式） x(F(x)G(x) （量詞分配等值式）（量詞分配等值式）或或 xF(x)xG(x) xF(x)x G(x) 量詞否定等值式量詞否定等值式 xF(x)y G(y) 換名規則換名規則 x y(F(x)G(y) 轄域收縮擴張規則轄域收縮擴張規則15求前束范式的實例求前束范式的

11、實例(3) xF(x)y(G(x,y)H(y)或或 xF(x)y(G(z,y)H(y) 代替規則代替規則 x y(F(x)(G(z,y)H(y) 解解 xF(x)y(G(x,y)H(y) zF(z)y(G(x,y)H(y) 換名規則換名規則 z y(F(z)(G(x,y)H(y) 轄域收縮擴張規則轄域收縮擴張規則165.3 一階邏輯的推論理論一階邏輯的推論理論推理的形式結構推理的形式結構1. A1 A2Ak B 若此式是永真式若此式是永真式, 則稱推理正確則稱推理正確, 記作記作A1 A2Ak B2. 前提前提: A1, A2, Ak 結論結論: B推理定理推理定理: 永真式的蘊涵式永真式的蘊

12、涵式17推理定理推理定理第一組第一組 命題邏輯推理定理的代換實例命題邏輯推理定理的代換實例 如如, xF(x)yG(y) xF(x) 第二組第二組 基本等值式生成的推理定理基本等值式生成的推理定理 如如, xF(x) xF(x), xF(x) xF(x) xF(x)x F(x), x F(x) xF(x)第三組第三組 其他常用推理定律其他常用推理定律 (1) xA(x)xB(x) x(A(x) B(x) (2) x(A(x) B(x)xA(x)xB(x) (3) x(A(x)B(x) xA(x)xB(x) (4) x(A(x)B(x) xA(x)xB(x)18量詞消去引入規則量詞消去引入規則1

13、. 全稱量詞消去規則全稱量詞消去規則( -) 或或 其中其中x,y是個體變項符號是個體變項符號, c是個體常項符號是個體常項符號, 且在且在A中中x不在不在 y和和 y的轄域內自由出現的轄域內自由出現.2. 全稱量詞引入規則全稱量詞引入規則( +) 其中其中x是個體變項符號是個體變項符號, 且不在前提的任何公式中自由出現且不在前提的任何公式中自由出現 xA(x)A(y) xA(x)A(c) A(x)xA(x)19量詞消去引入規則量詞消去引入規則3. 存在量詞消去規則存在量詞消去規則( -) 其中其中x是個體變項符號是個體變項符號, 且不在前提的任何公式和且不在前提的任何公式和B中自由中自由出現

14、出現 A(x)BxA(x)B20量詞消去引入規則量詞消去引入規則4. 存在量詞引入消去規則存在量詞引入消去規則( +) 或或 或或其中其中x,y是個體變項符號是個體變項符號, c是個體常項符號是個體常項符號, 且在且在A中中y和和c不在不在 x和和 x的轄域內自由出現的轄域內自由出現. BA(y)BxA(x) BA(c)BxA(x) A(y)xA(x) A(c)xA(x)21自然推理系統自然推理系統NL定義定義5.3 自然推理系統自然推理系統NL 定義如下定義如下:1. 字母表字母表. 同一階語言同一階語言L 的字母表的字母表2. 合式公式合式公式. 同同L 的合式公式的合式公式3. 推理規則

15、推理規則:(1) 前提引入規則前提引入規則(2) 結論引入規則結論引入規則(3) 置換規則置換規則(4) 假言推理規則假言推理規則(5) 附加規則附加規則(6) 化簡規則化簡規則(7) 拒取式規則拒取式規則22自然推理系統自然推理系統NL(8) 假言三段論規則假言三段論規則(9) 析取三段論規則析取三段論規則(10) 構造性二難推理規則構造性二難推理規則(11) 合取引入規則合取引入規則(12) -規則規則(13) +規則規則(14) -規則規則(15) +規則規則推理的證明推理的證明23構造推理證明的實例構造推理證明的實例例例5 在自然推理系統在自然推理系統NL 中構造下面推理的證明中構造下

16、面推理的證明, 取個體域取個體域R: 任何自然數都是整數任何自然數都是整數. 存在自然數存在自然數. 所以所以, 存在整數存在整數.解解 設設F(x):x是自然數是自然數, G(x):x是整數是整數.前提前提: x(F(x)G(x), xF(x)結論結論: xG(x)證明證明: x(F(x)G(x) 前提引入前提引入 F(x)G(x) - F(x)xG(x) + xF(x)xG(x) - xF(x) 前提引入前提引入 xG(x) 假言推理假言推理 24構造推理證明的實例構造推理證明的實例例例6 在自然推理系統在自然推理系統NL 中構造下面推理的證明中構造下面推理的證明, 取個體域取個體域R:

17、不存在能表示成分數的無理數不存在能表示成分數的無理數. 有理數都能表示成分數有理數都能表示成分數. 所以所以, 有理數都不是無理數有理數都不是無理數.解解 設設F(x):x是無理數是無理數, G(x):x是有理數是有理數, H(x):x能表示成分數能表示成分數.前提前提: x(F(x) H(x), x(G(x)H(x)結論結論: x(G(x)F(x) 證明證明: x(F(x) H(x) 前提引入前提引入 x( F(x)H(x) 置換置換 x(F(x)H(x) 置換置換 F(x)H(x) -25構造推理證明的實例構造推理證明的實例 x(G(x)H(x) 前提引入前提引入 G(x)H(x) - H

18、(x)F(x) 置換置換 G(x)F(x) 假言三段論假言三段論 x(G(x)F(x) +26重要提示重要提示yxyxF :),(要特別注意使用要特別注意使用 -、 +、 -、 +規則的條件規則的條件.反例反例1. 對對A= x yF(x,y)使用使用 -規則規則, 推得推得B= yF(y,y). 取解釋取解釋I: 個體域為個體域為R, 在在I下下A被解釋為被解釋為 x y(xy), 真真; 而而B被解釋為被解釋為 y(yy), 假假 原因原因: 在在A中中x自由出現自由出現在在 y的轄域的轄域F(x,y)內內反例反例2. 前提前提: P(x)Q(x), P(x) 結論結論: xQ(x) 取解

19、釋取解釋I: 個體域為個體域為Z, 在在I下前提為下前提為真真, 結論為假結論為假, 從而推理不正確從而推理不正確整除整除被被是偶數是偶數2:)(,:)(xxQxxP27反例反例2(續續)“證明證明”: P(x)Q(x) 前提引入前提引入 P(x) 前提引入前提引入 Q(x) 假言推理假言推理 xQ(x) +錯誤原因錯誤原因: 在使用在使用 +規則規則, 而而x在前提的公式中自由出現在前提的公式中自由出現.28第五章第五章 習題課習題課主要內容主要內容l 一階邏輯等值式一階邏輯等值式 基本等值式，置換規則、換名規則、代替規則基本等值式，置換規則、換名規則、代替規則l 前束范式前束范式l 推理的

20、形式結構推理的形式結構l 自然推理系統自然推理系統NL 推理定律、推理規則推理定律、推理規則29基本要求基本要求l 深刻理解并牢記一階邏輯中的重要等值式深刻理解并牢記一階邏輯中的重要等值式, 并能準確而熟并能準確而熟練地應用它們練地應用它們l 熟練正確地使用置換規則、換名規則、代替規則熟練正確地使用置換規則、換名規則、代替規則l 熟練地求出給定公式的前束范式熟練地求出給定公式的前束范式l 深刻理解自然推理系統深刻理解自然推理系統NL 的定義，牢記的定義，牢記NL 中的各條推理中的各條推理規則，特別是注意使用規則，特別是注意使用、 +、 +、 4條推理規則的條推理規則的條件條件l 能正確地給出有

21、效推理的證明能正確地給出有效推理的證明 30練習練習12 a1. 給定解釋給定解釋I如下如下:(1) 個體域個體域D=2,3(2) (3)(4)求下述在求下述在I下的解釋及其真值下的解釋及其真值: x y(F(f(x) G(y,f(a)2)3(, 3)2(:)( ffxf0)3 , 3(, 1)2 , 3()3 , 2()2 , 2(:),(1)3(, 0)2(:)( GGGGyxGFFxF解解 xF(f(x)yG(y,f(a) F(f(2) F(f(3) (G(2,f(2) G(3,f(2) 1 0 (1 0)031練習練習22.求下述公式的前束范式求下述公式的前束范式: xF(x)y(G(

22、x,y) H(x,y)解解 使用換名規則使用換名規則, xF(x)y(G(x,y) H(x,y) zF(z)y(G(x,y) H(x,y) z(F(z)y(G(x,y) H(x,y) z y(F(z)(G(x,y) H(x,y) 使用代替規則使用代替規則 xF(x)y(G(x,y) H(x,y) xF(x)y(G(z,y) H(z,y) x(F(x)y(G(z,y) H(z,y) x y(F(x)(G(z,y) H(z,y) 32練習練習33.構造下面推理的證明構造下面推理的證明:(1) 前提：前提： x(F(x)G(x), xF(x) 結論：結論： xG(x)證明：證明： x(F(x)G(x) 前提引入前提引入 F(y)G(y) xF(x) 前提引入前提引入 F(y) G(y) 假言推理假言推理 yG(y) + xG(x) 置換置換 33練習練習3(續續)(2) 前提：前提： x(F(x) G(x), xG(x)結論：結論： xF(x) 證明：用歸謬法證明：用歸謬法 xF(x) 結論否定引入結論否定引入 x F(x) 置換置換 xG(x) 前提引入前提引入 x G(x) 置換置換 x(F(x) G(x), 前提引入前提引入 F(c) G(c) F(c) G(c) G(c) 析取三段論析取三段論 G