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

1、Herbrand定理是經典邏輯中一條重要的元定理，它不僅為人工智能中的機器定理證明提供了理論基礎，更可以成為哥德爾完全性定理的替代物;此外，Herbrand定理還被應用于可判定問題，并取得了成果。盡管Herbrand定理本身有著良好的性質，但它的影響力仍然停留在經典邏輯中。誠然，在20世紀70年代至90年代早期，人們做過把Herbrand定理推廣到模態(tài)邏輯的各種嘗試，但都未能取得完全令人滿意的結果。直到1996年美國當代邏輯學家、證明論

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

3、erbrand定理范圍的有趣問題。但是Fitting后來不再從事這方面的研究工作，而且他本人也沒有指出在從其它的模態(tài)系統(tǒng)獲得“類似”的結果時會遇到哪些困難。本文力圖在充分考察Fitting工作的基礎上，嘗試給出其它一些模態(tài)系統(tǒng)的Herbrand定理，擴大模態(tài)Herbrand定理成果的范圍。概括說來，本文的工作包括以下三個方面。
　　第一，詳細闡述Fitting在探索模態(tài)邏輯領域的Herbrand定理方面所做的工作。在Fitting

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

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

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

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