王文龍，張博鋒(.喀什大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，中國(guó) 喀什 844000;.上海大學(xué)計(jì)算機(jī)工程與科學(xué)學(xué)院，中國(guó) 上海 0004)

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

王文龍1，張博鋒2
(1.喀什大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院，中國(guó) 喀什 844000;2.上海大學(xué)計(jì)算機(jī)工程與科學(xué)學(xué)院，中國(guó) 上海 200041)

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

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

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

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

1.1 不同表示形式

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

(1)

兩式成立的條件是：

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

b.在第二式中，c為任意個(gè)體常項(xiàng)；

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

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

(2)

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

1.2 實(shí)例比較與分析

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

對(duì)式(1),令A(yù)(x)=?yF(x,y)，F(xiàn)(x,y)表示x>y，則?xA(x)=?x?yF(x,y).在個(gè)體域?qū)崝?shù)集中，解釋為：對(duì)于任意的實(shí)數(shù)x都存在實(shí)數(shù)y，使得x>y，此命題為真.而由式(1)第一式有?x?yF(x,y)??yF(y,y)，可解釋為：存在實(shí)數(shù)y使得y>y，此命題為假.由此在推理中出現(xiàn)了由真推理假的情況，推理錯(cuò)誤.錯(cuò)誤原因主要是使用式(1)時(shí)，用來(lái)替代x的y在A(yíng)(x)=?yF(x,y)中約束出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿(mǎn)足條件(a)，即替代x的y應(yīng)為任意的不在A(yíng)(x)中約束出現(xiàn)的個(gè)體變項(xiàng).從另一個(gè)角度看，錯(cuò)誤的原因主要是在A(yíng)(x)=?yF(x,y)中，x在?y的轄域中自由出現(xiàn)，即x在指導(dǎo)變?cè)獃的轄域內(nèi)自由出現(xiàn)，因此為保證正確使用該推理規(guī)則，需滿(mǎn)足在A(yíng)中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(yíng)中x不在?y和?y的轄域中自由出現(xiàn)；而對(duì)于?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(yíng)中x不在?y和?y的轄域中自由出現(xiàn).

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

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

2.1 不同表示形式

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

(3)

該式成立的條件是：

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

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

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

(4)

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

2.2 實(shí)例比較與分析

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

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

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

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

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

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

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

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

3.1 不同表示形式

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

(5)

該式成立的條件是：

a.c是使A為真的特定的個(gè)體常項(xiàng)；

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

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

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

(6)

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

3.2 實(shí)例比較與分析

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

令A(yù)(x)=F(x,5)，表示x>5，在個(gè)體域整數(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)了由真推理假的情況，推理錯(cuò)誤，原因是替代x的c不能使A(c)=F(c,5)為真；若替代x的c取整數(shù)5，則A(c)=F(5,5)為假，由此在推理中出現(xiàn)了由真推理假的情況，推理錯(cuò)誤，此時(shí)錯(cuò)誤的原因是替代x的5在A(yíng)(c)=F(c,5)已經(jīng)出現(xiàn).因此，為保證正確使用該推理規(guī)則，需滿(mǎn)足條件(a)和(b)，即c是使A為真的特定的個(gè)體常項(xiàng)和c不在A(yíng)(x)中出現(xiàn).從另一角度看，兩種錯(cuò)誤的原因都是因?yàn)樘娲鷛的c不能保證A(c)=F(c,5)為真，因此，為保證正確使用該推理規(guī)則，需滿(mǎn)足條件(a).

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

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

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

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

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

4.1 不同表示形式

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

(7)

該式成立的條件是：

a.c是特定的個(gè)體常項(xiàng)；

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

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

(8)

(9)

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

4.2 實(shí)例比較與分析

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

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

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

不難發(fā)現(xiàn)此式可由式(8)第一式推導(dǎo)獲得，需滿(mǎn)足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íng)中y不在?x和?x的轄域中自由出現(xiàn)；而對(duì)于A(yíng)(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)為永真，需滿(mǎn)足在A(yíng)中y不在?x和?x的轄域中自由出現(xiàn)的條件.另外對(duì)該式亦可作如下推理：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)第二式，對(duì)其結(jié)論進(jìn)行等值演算，B→?xA(x)??x(B→A(x))(量詞轄域收縮與擴(kuò)張等值式)，此式成立要求B中不含x的出現(xiàn)，則式(9)第二式變?yōu)?/p>

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

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

5 量詞推理規(guī)則的標(biāo)準(zhǔn)形式

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

5.1 全稱(chēng)量詞消去規(guī)則的標(biāo)準(zhǔn)形式

(10)

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

5.2 全稱(chēng)量詞引入規(guī)則的標(biāo)準(zhǔn)形式

(11)

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

5.3 存在量詞消去規(guī)則的標(biāo)準(zhǔn)形式

(12)

該式成立的條件是：c是使A為真的特定的個(gè)體常項(xiàng).

5.4 存在量詞引入規(guī)則的標(biāo)準(zhǔn)形式

(13)

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

5.5 典型應(yīng)用實(shí)例

例1 前提：

結(jié)論：?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),

結(jié)論：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ù)學(xué)(修訂版)[M].北京：高等教育出版社，2004.

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

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

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

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

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

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

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

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

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

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

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

(編輯 HWJ)

重要啟事

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

本刊編輯部

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

國(guó)家自然科學(xué)基金項(xiàng)目(61561027)；新疆高?？蒲杏?jì)劃重點(diǎn)項(xiàng)目(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