王文龍，張博鋒(.喀什大學計算機科學與技術學院，中國 喀什 844000;.上海大學計算機工程與科學學院，中國 上海 0004)

一階邏輯推理系統(tǒng)中有關量詞推理規(guī)則的研究

王文龍1，張博鋒2
(1.喀什大學計算機科學與技術學院，中國 喀什 844000;2.上海大學計算機工程與科學學院，中國 上海 200041)

通過對兩種一階邏輯自然推理系統(tǒng)中有關量詞的推理規(guī)則及其成立條件的比較分析，給出形式簡單、直觀的有關量詞的推理規(guī)則和合理、嚴謹?shù)某闪l件，從而保證在使用這些規(guī)則時，既保留了直觀性，又消除了不嚴格性，并能準確把握成立條件.

一階邏輯；全稱量詞；存在量詞；推理規(guī)則；成立條件

文獻[1～12]描述了一階邏輯自然推理系統(tǒng)中有關量詞的推理規(guī)則，即全稱量詞引入規(guī)則、全稱量詞消去規(guī)則、存在量詞引入規(guī)則、存在量詞消去規(guī)則，在自然推理系統(tǒng)中具有重要作用.但由于使用這些推理規(guī)則時必須要滿足一定條件，而這些條件不容易準確把握.另一方面，關于量詞的推理規(guī)則，不同的自然推理系統(tǒng)會有不同的表示形式，使用這些規(guī)則的要求也有所不同.基于以上兩方面因素，在使用量詞的推理規(guī)則時，極易產(chǎn)生問題.因此，本文對兩種一階邏輯自然推理系統(tǒng)中有關量詞的推理規(guī)則及其成立條件進行比較分析，并根據(jù)分析，闡述在使用這些推理規(guī)則過程中應采取的表示形式及成立條件，從而保證在使用這些規(guī)則時，既保留規(guī)則的直觀性，又消除規(guī)則的不嚴格性，并能準確把握成立條件.

1 全稱量詞消去規(guī)則分析

1.1 不同表示形式

(1)在文獻[1]中的形式

(1)

兩式成立的條件是：

a.在第一式中，取代x的y應為任意的不在A(x)中約束出現(xiàn)的個體變項；

b.在第二式中，c為任意個體常項；

c.用y或c去取代A(x)中的自由出現(xiàn)的x時，一定要在x自由出現(xiàn)的一切地方進行取代.

(2)在文獻[2]中的形式

(2)

其中x,y是個體變項符號，c是個體常項符號，且在A中x不在?y和?y的轄域內自由出現(xiàn).

1.2 實例比較與分析

式(1)與式(2)形式一致，但成立條件描述不同.

對式(1),令A(x)=?yF(x,y)，F(xiàn)(x,y)表示x>y，則?xA(x)=?x?yF(x,y).在個體域實數(shù)集中，解釋為：對于任意的實數(shù)x都存在實數(shù)y，使得x>y，此命題為真.而由式(1)第一式有?x?yF(x,y)??yF(y,y)，可解釋為：存在實數(shù)y使得y>y，此命題為假.由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤.錯誤原因主要是使用式(1)時，用來替代x的y在A(x)=?yF(x,y)中約束出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿足條件(a)，即替代x的y應為任意的不在A(x)中約束出現(xiàn)的個體變項.從另一個角度看，錯誤的原因主要是在A(x)=?yF(x,y)中，x在?y的轄域中自由出現(xiàn)，即x在指導變元y的轄域內自由出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿足在A中x不在?y和?y的轄域中自由出現(xiàn)的條件.

式(2)推理規(guī)則形式化描述為：?xA(x)→A(y)為永真.證明如下：

?xA(x)→A(y)??xA(x)→A(x)(代替規(guī)則)，此等值式成立要求A(y)中不含x的出現(xiàn)，即在A中x不在?y和?y的轄域中自由出現(xiàn)；而對于?xA(x)→A(x)，若?xA(x)為真，則A(x)必為真，?xA(x)→A(x)為真；若?xA(x)為假，則?xA(x)→A(x)為真.因此?xA(x)→A(x)?1即?xA(x)→A(y)為永真，成立條件是在A中x不在?y和?y的轄域中自由出現(xiàn).

不難發(fā)現(xiàn)，式(1)和式(2)形式相同，成立條件是同一問題的不同描述.式(1)的條件直觀但更偏重于語義理解，式(2)的條件較嚴謹，是等值演算所要求的，與具體的解釋無關.

2 全稱量詞引入規(guī)則分析

2.1 不同表示形式

(1)在文獻[1]中的形式

(3)

該式成立的條件是：

a.無論A(y)中自由出現(xiàn)的個體變項y取何值，A(y)應該均為真；

b.取代自由出現(xiàn)的y的x，也不能在A(y)中約束出現(xiàn).

(2)在文獻[2]中的形式

(4)

其中x是個體變項符號，且不在前提的任何公式中自由出現(xiàn).

2.2 實例比較與分析

式(3)和式(4)形式略有不同，成立條件的描述也不同.

對式(3),令A(y)表示y是偶數(shù)，在個體域整數(shù)集中，解釋為：整數(shù)y是偶數(shù)，此解釋依據(jù)y的取值可為真亦可為假.而由式(3)有A(y)??xA(x)，?xA(x)可解釋為：所有整數(shù)都是偶數(shù)，此命題為假.由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤.錯誤原因是使用式(2)時，對于y取不同的值，A(y)可真可假，因此為保證正確使用該推理規(guī)則，需滿足條件(a)，即無論A(y)中自由出現(xiàn)的個體變項y取何值，A(y)應該均為真.

令A(y)=?xF(x,y)，F(xiàn)(x,y)表示x>y，在個體域實數(shù)集中，A(y)解釋為：對于實數(shù)y都存在實數(shù)x，使得x>y，此命題為真.而且對于任意的實數(shù)y，此命題均為真，滿足條件(a).而由式(3)有，A(y)??xA(x),?xA(x)=?x?xF(x,x)，可解釋為：對于任意的實數(shù)x，存在實數(shù)x使得x>x，此命題為假.由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤.原因主要是使用式(3)時，用來替代y的x在A(y)=?xF(x,y)中約束出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿足條件(b)，即取代自由出現(xiàn)的y的x，也不能在A(y)中約束出現(xiàn).從另一個角度看，錯誤的原因是當y的值取x時，不能保證A(x)=?xF(x,x)為真，因此，為保證正確使用該推理規(guī)則，需滿足條件(a).

使用式(4)有如下推理證明：前提：P(x)→Q(x),P(x).結論：?xQ(x).

證明：①P(x)→Q(x) ②P(x) ③Q(x) ④?xQ(x)(式(4)).

給出此推理的一個解釋，在個體域整數(shù)集中，P(x)表示x是偶數(shù)，Q(x)表示x被2整除.則P(x)→Q(x)為真，P(x)真值不確定，?xQ(x)為假，因此此推理錯誤.原因是在③推理④的過程中，使用式(4)時，x在前提中自由出現(xiàn).因此為保證正確使用該推理規(guī)則，需滿足x不在前提的任何公式中自由出現(xiàn)的條件.

對比式(3)和式(4)，可對式(3)做如下演算：A(y)?A(x)(代替規(guī)則)，此等值式成立要求A(y)中不含x的出現(xiàn)，此時，式(3)可改為A(y)?A(x)??xA(x)，即為式(4)，兩式在滿足A(y)中不含x的出現(xiàn)的條件時是相同的.不難看出，式(4)使用時所需條件不完備，而且可以由式(3)推導出，因此，完全可以用式(3)替代式(4).

3 存在量詞消去規(guī)則分析

3.1 不同表示形式

(1)在文獻[1]中的形式

(5)

該式成立的條件是：

a.c是使A為真的特定的個體常項；

b.c不在A(x)中出現(xiàn)；

c.A(x)中除自由出現(xiàn)的x外，還有其他自由出現(xiàn)的個體變項，此規(guī)則不能使用.

(2)在文獻[2]中的形式

(6)

其中x是個體變項符號, 且不在前提的任何公式和B中自由出現(xiàn).

3.2 實例比較與分析

式(5)和式(6)形式不同，成立條件的描述也不同.

令A(x)=F(x,5)，表示x>5，在個體域整數(shù)集中，?xA(x)解釋為：存在整數(shù)x>5，此命題為真.而由式(5)有?xA(x)?A(c)，若替代x的c取大于5的整數(shù)，則A(c)=F(c,5)為真，推理正確；若替代x的c取小于5的整數(shù)，則A(c)=F(c,5)為假，由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤，原因是替代x的c不能使A(c)=F(c,5)為真；若替代x的c取整數(shù)5，則A(c)=F(5,5)為假，由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤，此時錯誤的原因是替代x的5在A(c)=F(c,5)已經(jīng)出現(xiàn).因此，為保證正確使用該推理規(guī)則，需滿足條件(a)和(b)，即c是使A為真的特定的個體常項和c不在A(x)中出現(xiàn).從另一角度看，兩種錯誤的原因都是因為替代x的c不能保證A(c)=F(c,5)為真，因此，為保證正確使用該推理規(guī)則，需滿足條件(a).

令A(x)=F(x,y)，F(xiàn)(x,y)表示x>y，在個體域實數(shù)集中，?xA(x)=?xF(x,y)解釋為：存在實數(shù)x，使得x>y，此命題為真.而由式(5)有?xA(x)?A(c)?F(c,y)，顯而易見，F(xiàn)(c,y)為假，由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤.原因是在A(x)=F(x,y)中，除了自由出現(xiàn)的x外還有自由出現(xiàn)的y，因此，為保證正確使用該推理規(guī)則，需滿足條件(c)，即A(x)中除自由出現(xiàn)的x外，還有其他自由出現(xiàn)的個體變項，不能使用此規(guī)則.從另一角度看，錯誤的原因是因為替代x的c不能保證A(c)=F(c,y)為真，因此，為保證正確使用該推理規(guī)則，需滿足條件(a).

對式(6)結論進行等值演算，?xA(x)→B??x(A(x)→B)(量詞轄域收縮與擴張等值式)，此式成立要求B中不含x的出現(xiàn)，則式(6)變?yōu)?/p>

不難發(fā)現(xiàn)此式可由式(4)獲得，需滿足x不在前提的任何公式和B中自由出現(xiàn)的條件.另外，式(6)從形式上看，前提不含?量詞，結論含?量詞，與存在量詞消去的含義不符.

對比式(5)和式(6)，不論從形式還是語義上看，式(5)更具有存在量詞消去的含義，而成立條件(b)和(c)可以由條件(a)替代.

4 存在量詞引入規(guī)則分析

4.1 不同表示形式

(1)在文獻[1]中的形式

(7)

該式成立的條件是：

a.c是特定的個體常項；

b.取代c的x不能在A(c)中出現(xiàn)過.

(2)在文獻[2]中的形式

(8)

(9)

其中x,y是個體變項符號,c是個體常項符號, 且在A中y和c不在?x和?x轄域內自由出現(xiàn).

4.2 實例比較與分析

式(7)和式(9)第一式形式相同，但成立條件的描述不同.而式(8)形式更加多樣.

對式(7)，令A(c)=?xF(x,c)，F(xiàn)(x,c)表示x>c，在個體域實數(shù)集中，A(c)解釋為：存在實數(shù)x>c，此命題為真.而由式(7)有A(c)??xA(x)，?xA(x)=?x?xF(x,x)，可解釋為：存在實數(shù)x>x，此命題為假.由此在推理中出現(xiàn)了由真推理假的情況，推理錯誤.原因主要是使用式(7)時，用來替代c的x在A(c)=?xF(x,c)中出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿足條件(b)，即取代c的x，不能在A(c)中出現(xiàn).從另一個角度看，錯誤的原因主要是在A(c)=?xF(x,c)中，c在?x的轄域中自由出現(xiàn)，即c在指導變元x的轄域內自由出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿足在A中c不在?x和?x的轄域中自由出現(xiàn)的條件.

對式(8)第二式其結論進行等值演算，B→?xA(x)??x(B→A(x))(量詞轄域收縮與擴張等值式)，此式成立要求B中不含x的出現(xiàn)，則式(8)第二式變?yōu)椋?/p>

不難發(fā)現(xiàn)此式可由式(8)第一式推導獲得，需滿足B中不含x出現(xiàn)的條件.

再分析式(8)第一式，該推理規(guī)則形式化描述為：A(y)→?xA(x)為永真.證明如下：A(y)→?xA(x)?A(y)→?yA(y)(換名規(guī)則)，此等值式成立要求A(x)中不含y的出現(xiàn)，即在A中y不在?x和?x的轄域中自由出現(xiàn)；而對于A(y)→?yA(y)，若A(y)為真，則?yA(y)必為真，A(y)→?yA(y)為真；若A(y)為假，則A(y)→?yA(y)為真.因此A(y)→?yA(y)?1，即A(y)→?xA(x)為永真，需滿足在A中y不在?x和?x的轄域中自由出現(xiàn)的條件.另外對該式亦可作如下推理：A(y)??xA(x)?A(c)??xA(x)，推理中依次用到式(3)、式(1)第二式、式(8)(或式(9)第一式)，亦可有如下推理：A(y)??xA(x)??xA(x)，推理中依次用到式(3)和?xA(x)??xA(x)(?xA(x)→?xA(x)?A(x)∨?xA(x)?1).

最后分析式(9)第二式，對其結論進行等值演算，B→?xA(x)??x(B→A(x))(量詞轄域收縮與擴張等值式)，此式成立要求B中不含x的出現(xiàn)，則式(9)第二式變?yōu)?/p>

不難發(fā)現(xiàn)此式可由式(9)第一式獲得，需滿足B中不含x出現(xiàn)的條件.

從上分析可以看出，盡管式(8)、式(9)形式多樣，但完全可以用式(7)或式(9)第一式替代.對比式(7)，式(9)第一式與其形式相同，成立條件與式(7)的條件(b)是同一問題的不同描述，即在A中c不在?x和?x的轄域中自由出現(xiàn).

5 量詞推理規(guī)則的標準形式

通過以上的分析，可以給出形式簡單、直觀的有關量詞的推理規(guī)則，也可以給出合理、嚴謹?shù)某闪l件.

5.1 全稱量詞消去規(guī)則的標準形式

(10)

兩式成立的條件是：其中x,y是個體變項符號，c是個體常項符號，且在A中x不在?y和?y的轄域內自由出現(xiàn).

5.2 全稱量詞引入規(guī)則的標準形式

(11)

該式成立的條件是：無論A(y)中自由出現(xiàn)的個體變項y取何值，A(y)應該均為真.

5.3 存在量詞消去規(guī)則的標準形式

(12)

該式成立的條件是：c是使A為真的特定的個體常項.

5.4 存在量詞引入規(guī)則的標準形式

(13)

該式成立的條件是：在A中c不在?x和?x轄域內自由出現(xiàn).

5.5 典型應用實例

例1 前提：

結論：?x(G(x)→f(x)).

②?x(F(x)∨H(x)), ①

③?x(H(x)→F(x)), ②

④H(y)→F(y), 式(10)

⑤?x(G(x)→H(x)),

⑥G(y)→H(y), 式(10)

⑦G(y)→F(y), ⑥④

⑧?x(G(x)→F(x)). 式(11)

例2 前提：

?x(P(x)→(Q(y)∧R(x))),?xP(x),

結論：Q(y)∧?x(P(x)∧R(x)).

證 ①?xP(x),

②P(c), 式(12)

③?x(P(x)→(Q(y)∧R(x))),

④(P(c)→(Q(y)∧R(c))), 式(10)

⑤Q(y)∧R(c), ②④

⑥Q(y),

⑦R(c),

⑧P(c)∧R(c), ②⑦

⑨?x(P(x)∧R(x)), 式(13)

⑩Q(y)∧?x(P(x)∧R(x)). ⑥⑨

[1] 耿素云，屈婉玲.離散數(shù)學(修訂版)[M].北京：高等教育出版社，2004.

[2] 屈婉玲，耿素云，張立昂.離散數(shù)學[M].北京：高等教育出版社，2008.

[3] 耿素云，屈婉玲，王悍貧.離散數(shù)學教程[M].北京：北京大學出版社，2004.

[4] 傅 彥，顧小豐，王慶先,等.離散數(shù)學及其應用[M].北京：高等教育出版社，2007.

[5] 魏雪梅. 離散數(shù)學及其應用[M].北京：機械工業(yè)出版社，2008.

[6] 方世昌.離散數(shù)學(第三版)[M].西安：西安電子科技大學出版社，2009.

[7] 楊圣洪，張英杰，陳義明. 離散數(shù)學[M].北京：科學出版社，2011.

[8] 苑成存. 一種可行的量化邏輯自然演繹系統(tǒng)[J]. 洛陽大學學報，2002，17(3)：30-33.

[9] 孟令江. 一階邏輯推理系統(tǒng)F下量詞的性質及運算規(guī)律[J]. 河北大學學報(自然科學版)，2008，28(1)：18-21.

[10] 邱文. 一階邏輯推理有效性的探析[J]. 海南大學學報(自然科學版)，2006，24(2):104-106.

[11] 何自強. 離散數(shù)學中與量詞有關的推理規(guī)則[J]. 北京航空航天大學學報，2000，26(4)：432-434.

[12] 潘美芹，丁志軍，王永麗. 謂詞邏輯推理中證明方法的判定[J]. 山東科技大學學報(自然科學版)，2005，24(4)：84-86.

(編輯 HWJ)

重要啟事

“優(yōu)先數(shù)字出版”是以紙質版期刊錄用稿件為出版內容，先于紙質期刊出版日期出版的數(shù)字期刊出版方式．我刊已于2012年起與中國學術期刊(光盤版)電子雜志社簽訂了優(yōu)先數(shù)字出版協(xié)議．凡被我刊錄用的稿件一經(jīng)優(yōu)先數(shù)字出版，讀者即可在中國知網(wǎng)(CNKI)全文數(shù)據(jù)庫進行檢索和下載．凡向本刊投稿的作者，如無特別申明，均被視為作者授權本刊編輯部在紙質期刊出版前，可以在中國學術期刊(光盤版)電子雜志社主辦的“中國知網(wǎng)”(www.cnki.net)上優(yōu)先數(shù)字出版；也被視為作者同意并授權我刊與其他電子雜志社簽訂的協(xié)議，并許可其在全球范圍內使用該文的信息網(wǎng)絡傳播權、數(shù)字化復制權、數(shù)字化匯編權、發(fā)行權及翻譯權，并不再額外支付稿酬．

本刊編輯部

Study of Inference Rules for Quantifiers in First-order Logic Inference System

WANGWen-long1*,ZHANGBo-feng2
(1.College of Computer Science and Technology, Kashgar University, Kashgar 844000, China;2.School of Computer Engineering and Science, Shanghai University, Shanghai 200041, China)

Through the analysis of two inference rules for quantifiers and establishing conditions in first-order logic natural inference system, in this work, we establish intuitive inference rules for quantifiers with reasonable and strictly elaborated conditions. Not only these rules are intuitive and strict, but they also establish conditions that can accurately be grasped.

first order logic; universal quantifier; existential quantifier; inference rules; establish condition

2016-05-04

國家自然科學基金項目(61561027)；新疆高?？蒲杏媱澲攸c項目(XJEDU2014I039)

10.7612/j.issn.1000-2537.2017.03.016

TP301 O141

A

1000-2537(2017)03-0089-06

*通訊作者,E-mail：wwl-yx@163.com