模態(tài)HERBRAND定理研究.pdf

1、Herbrand定理是經(jīng)典邏輯中一條重要的元定理，它不僅為人工智能中的機(jī)器定理證明提供了理論基礎(chǔ)，更可以成為哥德?tīng)柾耆远ɡ淼奶娲?此外，Herbrand定理還被應(yīng)用于可判定問(wèn)題，并取得了成果。盡管Herbrand定理本身有著良好的性質(zhì)，但它的影響力仍然停留在經(jīng)典邏輯中。誠(chéng)然，在20世紀(jì)70年代至90年代早期，人們做過(guò)把Herbrand定理推廣到模態(tài)邏輯的各種嘗試，但都未能取得完全令人滿意的結(jié)果。直到1996年美國(guó)當(dāng)代邏輯學(xué)家、證明論

2、專家Fitting的工作，模態(tài)邏輯領(lǐng)域的Herbrand定理才取得突破性進(jìn)展。Fitting通過(guò)把“謂詞抽象”這一裝置引入通常的一階模態(tài)邏輯，以一種很自然的方式加強(qiáng)了一階模態(tài)邏輯語(yǔ)言的表達(dá)力，從而獲得一個(gè)沒(méi)有Barcan公式的模態(tài)系統(tǒng)K的Herbrand定理，這是迄今為止與經(jīng)典Herbrand定理最為接近的一種模態(tài)Herbrand定理形式。
　　后來(lái)Fitting又指出:類似的結(jié)果也可以從其它的模態(tài)系統(tǒng)獲得，這是一個(gè)可以解決模態(tài)H

3、erbrand定理范圍的有趣問(wèn)題。但是Fitting后來(lái)不再?gòu)氖逻@方面的研究工作，而且他本人也沒(méi)有指出在從其它的模態(tài)系統(tǒng)獲得“類似”的結(jié)果時(shí)會(huì)遇到哪些困難。本文力圖在充分考察Fitting工作的基礎(chǔ)上，嘗試給出其它一些模態(tài)系統(tǒng)的Herbrand定理，擴(kuò)大模態(tài)Herbrand定理成果的范圍。概括說(shuō)來(lái)，本文的工作包括以下三個(gè)方面。
　　第一，詳細(xì)闡述Fitting在探索模態(tài)邏輯領(lǐng)域的Herbrand定理方面所做的工作。在Fitting

4、的論文中，由于篇幅有限，許多重要定理的證明過(guò)程和許多重要的轉(zhuǎn)換規(guī)則、轉(zhuǎn)換步驟都被省略掉了。本文力圖將它們補(bǔ)充完整，為后面探索其它模態(tài)系統(tǒng)的Herbrand定理工作做好準(zhǔn)備。首先，給出了模態(tài)邏輯的Skolem化定理的詳細(xì)證明過(guò)程，可以說(shuō)這一定理是Fitting所有工作的精華之處，關(guān)系到整個(gè)模態(tài)邏輯領(lǐng)域Herbrand定理的成敗。其次，給出了加標(biāo)公式表列系統(tǒng)K的可靠性和完全性的詳細(xì)證明過(guò)程，為模態(tài)系統(tǒng)K的Herbrand定理從左到右方向的證

5、明做好準(zhǔn)備。再次，在給出模態(tài)Herbrand膨脹的矢列演算規(guī)則中，補(bǔ)充了合取規(guī)則、析取規(guī)則和可能算子規(guī)則。最后，給出了在加標(biāo)公式表列系統(tǒng)K中，從公式X的表列證明序列構(gòu)造X的不含量詞的Herbrand變形證明序列的詳細(xì)轉(zhuǎn)換步驟。
　　第二，給出了沒(méi)有Barcan公式的模態(tài)系統(tǒng)D、T、S4的Herbrand定理及詳細(xì)證明過(guò)程。首先，給出模態(tài)系統(tǒng)D、T、S4的系統(tǒng)有效概念，并證明模態(tài)邏輯中的Skolem化步驟和Herbrand膨脹步驟保

6、持系統(tǒng)有效性，即D(T、S4)系統(tǒng)的有效式經(jīng)過(guò)Skolem化步驟和Herbrand膨脹步驟后仍是D(T、S4)系統(tǒng)的有效式。這樣就可以獲得模態(tài)系統(tǒng)D、T、S4的Herbrand定理并完成這些定理從右到左方向的證明工作。其次，在考慮謂詞抽象的加標(biāo)公式表列系統(tǒng)K的基礎(chǔ)上增加相應(yīng)的擴(kuò)展規(guī)則分別獲得加標(biāo)公式表列系統(tǒng)D、T、S4，并證明它們的可靠性和完全性，為這些系統(tǒng)的Herbrand定理從左到右方向的證明做好準(zhǔn)備。最后，給出了在加標(biāo)公式表列系統(tǒng)

7、D、T、S4中，從公式X的表列證明序列構(gòu)造X的不含量詞的Herbrand變形證明序列的詳細(xì)轉(zhuǎn)換步驟。
　　第三，對(duì)謂詞抽象進(jìn)行了系統(tǒng)的哲學(xué)考察。謂詞抽象是Fitting探索模態(tài)Herbrand定理工作取得成功的關(guān)鍵，有必要對(duì)它作進(jìn)一步的研究，本文從哲學(xué)角度對(duì)謂詞抽象進(jìn)行了深入地考察。首先，考察了謂詞抽象被引入模態(tài)邏輯的哲學(xué)背景。當(dāng)羅素使用的“初現(xiàn)”/“乍現(xiàn)”(primary occurrences)和“再現(xiàn)”（secondary