杜國平

（中國社會科學院哲學研究所，北京100732）

知識蘊涵直覺主義邏輯系統(tǒng)

杜國平

（中國社會科學院哲學研究所，北京100732）

在知識蘊涵命題邏輯的基礎(chǔ)上，借助強知識蘊涵，可以構(gòu)建知識蘊涵直覺主義邏輯系統(tǒng)。結(jié)合知識蘊涵邏輯和直覺主義邏輯的形式語義，可以證明知識蘊涵直覺主義邏輯系統(tǒng)具有可靠性和完全性。在該系統(tǒng)中，矛盾律仍然成立，但是排中律、雙重否定消去律、司各脫法則都不再成立。在該系統(tǒng)中，弗協(xié)調(diào)邏輯和直覺主義邏輯的基本特征都被保留了下來，該系統(tǒng)給出了一個處理矛盾問題的既是弗協(xié)調(diào)的、又是直覺主義的兼容方案。

知識蘊涵；直覺主義；司各脫法則；矛盾

為了解決包含不協(xié)調(diào)信息的知識系統(tǒng)的推理問題，我們建立了知識蘊涵邏輯的命題邏輯系統(tǒng)、模態(tài)邏輯系統(tǒng)、時態(tài)邏輯系統(tǒng)以及謂詞邏輯系統(tǒng)［1－9］，本文將在上述工作的基礎(chǔ)上，在強知識蘊涵的基礎(chǔ)上將知識蘊涵邏輯推廣到直覺主義邏輯系統(tǒng)之中，建立知識蘊涵直覺主義命題邏輯系統(tǒng)。在該系統(tǒng)中，我們希望基本的直覺主義邏輯思想在其中得以體現(xiàn)，即排中律、雙重否定消去律等在其中不是定理；當然，我們也希望在該系統(tǒng)中不矛盾律仍然是定理，但是司各脫法則不是定理，即弗協(xié)調(diào)邏輯的特征在該系統(tǒng)中仍然得以保持。

一、形式語言

定義1.1 知識蘊涵直覺主義命題邏輯的形式語言LIP和知識蘊涵命題邏輯語言基本相同，只是增加了一個初始符合∨。包括下列三類初始符號：

形式語言LIP中的第一類符號稱為命題符號，第二類符號是命題聯(lián)結(jié)詞符號，第三類符號是左右括號。初始符號組成的有窮序列稱為符，全體符所形成的集合記為Expr（LIP）。

定義1.2 LMP中的一個表達式是原子公式，當且僅當它是一個單獨的命題符號。

由LIP中所有原子公式構(gòu)成的集合記為Atom（LIP）。我們用大寫字母A、B、C、D等表示任意的公式，用符號Σ、Γ、Δ等表示任意的公式集，由LIP中所有公式構(gòu)成的集合記為Form（LIP）。

定義1.3 （Form（LIP））A∈Form（LIP），當且僅當它能（有窮次）由下列規(guī)則而得：

［1］Atom（LIP）?Form（LIP）；

［2］如果A∈Form（LIP），則（ A）∈Form（LIP）；

［3］如果A、B∈Form（LIP），那么（A∧B）∈Form（LIP）、（A∨B）∈Form（LIP）、（A→B）∈Form（LIP）。

括號省略規(guī)則與經(jīng)典命題邏輯相同。

定理1.1（公式歸納原理） 令P是關(guān)于符的一個性質(zhì)。如果：

［1］對于任何命題符p，P（p）；

［2］如果P（A）成立，則P（A）成立；

［3］如果P（A）、P（B）成立，則P（A∧B）、P（A∨B）、P（A→B）也都成立。

那么所有公式都具有性質(zhì)P。

其他聯(lián)結(jié)詞通過定義給出：

定義1.4 設(shè)A∈Form（LIP），Atomic（A）定義如下：

［1］如果A是原子公式，那么Atomic（A）＝｛A｝；

［2］如果A＝ B，那么Atomic（A）＝Atomic（B）；

［3］如果A＝B∧C，那么Atomic（A）＝Atomic（B）∪Atomic（C）；

［4］如果A＝B∨C，那么Atomic（A）＝Atomic（B）∪Atomic（C）；

［5］如果A＝B→C，那么Atomic（A）＝Atomic（B）∪Atomic（C）。

定義1.5 假設(shè)A、B是公式，稱A、B相關(guān)，當且僅當

二、知識蘊涵直覺主義命題邏輯公理系統(tǒng)ID

定義2.1 知識蘊涵直覺主義命題邏輯公理系統(tǒng)ID的公理是下列形式的公式：

系統(tǒng)ID的推理規(guī)則只有一條，即分離規(guī)則（modus ponens）：由A和A→B可以推出B。簡記為MP。

定義2.2 公式A由公式集Σ形式可推演，當且僅當存在公式序列：

使得An＝A，并且每一個Ak（1≤k≤n）滿足下列條件之一：

［1］Ak是公理；

［2］Ak∈Σ；

［3］有i，j＜k，使得Ai＝Aj→Ak。

如果公式A由公式集Σ形式可推演，則稱Σ可推演出A，符號記為Σ├IDA，也簡記為：Σ├A

定義2.3 如果公式A由?形式可推演，則稱公式A是可證明的。由?到A形式可推演的一個公式序列稱為公式A的一個證明。如果公式A是可證明的，則稱公式A為系統(tǒng)ID的定理，符號記為├IDA，也簡記為：├A。為了與其它的定理相區(qū)別，在下文中，我們將系統(tǒng)ID內(nèi)的定理記為IDTh。

三、知識蘊涵直覺主義邏輯的形式語義

定義3.1 設(shè)LIP是一知識蘊涵直覺主義命題邏輯的形式語言，一個克里普克模型（簡稱模型）是一個三元組〈W，R，V〉，其中

［1］W是一個非空集，

［2］R?W×W，對于任意的w1，w2，w3∈W，w1Rw1，并且，若w1Rw2，w2Rw3，則w1Rw3；

［3］V：Atomic（LIP）×W→｛1，0｝，并且滿足：對任一原子公式A，若w1Rw2，則V（A，w1）≤V（A，w2）。

［1］對任一原子公式A，V（A，w）∈｛1，0｝；

［3］V（A∧B，w）＝1，當且僅當V（A，w）＝1并且V（B，w）＝1；

［4］V（A∨B，w）＝1，當且僅當V（A，w）＝1或者V（B，w）＝1；

［5］如果對于任一w′∈W，若wRw′，當V（A，w′）＝V（B，w′），或者V（A，w′）＝0，V（B，w′）＝1，且A、B相關(guān)時，那么，V（A→B，w）＝1；

［6］如果存在w′∈W，wRw′，當V（A，w′）＝1，V（B，w′）＝0，或者V（A，w′）＝0，V（B，w′）＝1，且A、B不相關(guān)時，那么V（A→B，w）＝0。

［1］V（A，w）∈｛1，0｝；

［2］對于任意的w、w′∈W，如果wRw′并且V（A，w）＝1，那么V（A，w′）＝1。

定義3.3 設(shè)Σ?Form（LIP），A∈Form（LIP）。

Σ╞╱A表示Σ╞A不成立。

定理3.2 設(shè)A，B，C∈Form（LIP），

定理3.3 如果Σ╞A，并且Σ╞A→B，則Σ╞B。

四、ID的元理論

定理4.1 設(shè)Σ?Form（LIP），A∈Form（LIP）。

［1］如果├A，則╞A；

［2］如果Σ├A，則Σ╞A。

證明：

［1］施歸納于證明的結(jié)構(gòu)。這只需證明形式系統(tǒng)ID中的公理都是有效的，并且其推理規(guī)則都是保持有效的。定理3.2和定理3.3已經(jīng)證明了這兩點。

［2］是［1］的推論。

定義4.1 設(shè)Σ?Form（LIP），Σ是ID協(xié)調(diào)的，當且僅當存在公式A，使得Σ├╱IDA。

為了方便，Σ是ID協(xié)調(diào)的也簡稱Σ是協(xié)調(diào)的。

根據(jù)Ax14，顯然有：對于任一公式B，如果Σ是協(xié)調(diào)的，那么B和 B至少有一個不屬于Σ。

定義4.2（強協(xié)調(diào)性） 設(shè)Σ?Form（LIP），Σ是強協(xié)調(diào)的，當且僅當Σ滿足下列條件：

［1］Σ是協(xié)調(diào)的；

［2］對于任何A∈Form（LIP），Σ├IDA蘊涵A∈Σ；

［3］對于任何A、B∈Form（LIP），A∨B∈Σ蘊涵A∈Σ或B∈Σ。

定理4.2 設(shè)Σ?Form（LIP），A∈Form（LIP），并且Σ├╱IDA。于是Σ可以擴充為Σ′?Form（L′），使得Σ′是強協(xié)調(diào)集，并且Σ′├╱IDA。

證明：

因為形式語言LIP是一可數(shù)語言，所以令

（1）B0，B1，…，Bn，Bn＋1，…

是Form（LIP）中公式的任意一個排列。

定義一個Σn?Form（LIP）的無限序列如下：

令Σ0＝Σ。由Σn構(gòu)造Σn＋1的規(guī)則如下：

［1］如果Σn，Bn├IDA，則令Σn＋1＝Σn；

［2］如果Σn，Bn├╱IDA，并且Bn不是析取式，則令Σn＋1＝Σn∪｛Bn｝；

［3］如果Σn，Bn├╱IDA，并且Bn是析取式B′n∨B″n，則有

或者Σn，Bn′├╱IDA

或者Σn，Bn″├╱IDA

令

顯然，有

（2）對于任意的n∈ω，Σn?Σn＋1

（3）對于任意的n∈ω，Σn├╱IDA

證明：

（4）Σ′├╱I DA

（5）Σ′具有強協(xié)調(diào)性。

首先證明（4）。假設(shè)Σ′├IDA。于是存在Σ′的有限子集｛A1，…，Ak｝使得A1，…，Ak├IDA。令，假設(shè)i＝max（i1，…，ik），則A1，…，Ak?Σi，因而有Σi├IDA，這與（3）矛盾。因此Σ′├╱IDA。

下面證明（5）。

因為存在公式A，Σ′├╱IDA，所以Σ′是協(xié)調(diào)的。這樣Σ′滿足了強協(xié)調(diào)性的第一個條件。

設(shè)B∈Form（LID）并且Σ′├IDB。則有：

（6）Σ′，B├╱I DA

因為如果Σ′，B├IDA，則有Σ′├IDB→（B→A），進而有Σ′├ICA，這與（4）矛盾。

設(shè)公式B在排列（1）中為Bm，則有

（7）Σm，Bm├╱IDA

因為如果Σm，Bm├IDA，則由于Σm?Σ′，故有Σ′，B├IDA，這與（6）矛盾。

根據(jù)由Σn構(gòu)造Σn＋1的規(guī)則［2］～［4］可知Bm∈Σm＋1，因此有B∈Σ′，于是Σ′滿足了強協(xié)調(diào)性的第二個條件。

設(shè)B′∨B″∈Σ′并且B′∨B″在排列（1）中為Bm。于是

（8）Σm，B′∨B″├╱IDA

因為如果Σm，B′∨B″├IDA，則Σ′，B′∨B″├IDA，則有Σ′├IDB′∨B″→（B′∨B″→A），進而有Σ′├IDA，這與（4）矛盾。

根據(jù)由Σn構(gòu)造Σn＋1的規(guī)則［3］可知：或者B′∈Σm＋1或者B″∈Σm＋1，因此或者B′∈Σ′或者B″∈Σ′，于是Σ′滿足了強協(xié)調(diào)性的第三個條件。

這樣就證明了Σ′具有強協(xié)調(diào)性。

設(shè)Σ?Form（LIP）、A∈Form（LIP），并且Σ├╱IDA。令Σ0＝Σ。由定理4.2可知，Σ0可擴充為Σ1?Form（LIP），使得Σ1是強協(xié)調(diào)的并且Σ1├╱IDA。同樣，Σ1可擴充為Σ2?Form（LIP），使得Σ2是強協(xié)調(diào)的并且Σ2├╱IDA，……。這樣，對于任一n≥1，有Σn?Form（LIP），使得Σn是強協(xié)調(diào)的并且Σn├╱IDA，并且Σn?Σn＋1。

定義4.3 設(shè)Σ├╱IDA，與Σ、A相關(guān)的三元組m＊＝＜W＊，R＊，V＊＞是按照如下方式給出的。

W＊＝｛wn｜Σ?wn，wn是強協(xié)調(diào)的并且wn├╱IDA｝；

wiR＊wj當且僅當i≤j；

對于任一原子公式B，V＊（B，wn）＝1當且僅當B∈wn。

定理4.3 設(shè)Σ├╱IDA，m＊＝＜W＊，R＊，V＊＞是與Σ、A相關(guān)的三元組，wi、wj∈W＊。

［1］對所有的w、w′、w″∈W＊，wR＊w并且wR＊w′∧w′R＊w″→wR＊w″；

［2］對所有的w、w′∈W＊，wR＊w′→w?w′。

定理4.4 設(shè)Σ├╱IDA，m＊＝＜W＊，R＊，V＊＞是與Σ、A相關(guān)的三元組，D∈Form（LIP）。那么，對于任意的n（≥1），V＊（D，wn）＝1?D∈wn。

證明：

［1］當D為原子公式，則由V＊的定義可知，命題成立。

［3］當D為B∨C時。

先證B∨C∈wn?V＊（B∨C，wn）＝1

B∨C∈wn?B∈wn或者C∈wn（wn是強協(xié)調(diào)的之析取性）

?V＊（B，wn）＝1或者V＊（C，wn）＝1（歸納假設(shè)）

?V＊（B∨C，wn）＝1（語義定義）

再證V＊（B∨C，wn）＝1?B∨C∈wn

V＊（B∨C，wn）＝1?V＊（B，wn）＝1或者V＊（C，wn）＝1（語義定義）

?B∈wn或者C∈wn（歸納假設(shè)）

?B∨C∈wn（wn是強協(xié)調(diào)的之形式推演封閉性）

［4］當D為B∧C時。

先證B∧C∈wn?V＊（B∧C，wn）＝1

B∧C∈wn?B∈wn而且C∈wn（wn是強協(xié)調(diào)的之形式推演封閉性）

?V＊（B，wn）＝1而且V＊（C，wn）＝1（歸納假設(shè)）

?V＊（B∧C，wn）＝1（語義定義）

再證V＊（B∧C，wn）＝1?B∧C∈wn

V＊（B∧C，wn）＝1?V＊（B，wn）＝1而且V＊（C，wn）＝1（語義定義）

?B∈wn而且C∈wn（歸納假設(shè)）

?B∧C∈wn（wm是強協(xié)調(diào)的之形式推演封閉性）

［5］當D為B→C時。

假設(shè)V＊（D，wn）＝1：

（1）如果對于任一wm∈W，若wnRwm，則V（B，wm）＝V（C，wm），那么根據(jù)歸納假設(shè)有：B∈wm當且僅當C∈wm，因為wnRwn，所以有B∈wn當且僅當C∈wn，即或者B∈wn且C∈wn，或者B?wn且C?wn，亦即有或者B∈wn且C∈wn，或者 B∈wn且C∈wn。這樣，或者有wn├B且wn├C或者有wn├ B且wn├ C，那么根據(jù)公理2和公理3，均可得到：wn├B→C，因為wn是強協(xié)調(diào)集，所以有（B→C）∈wn。

（2）如果對于任一wm∈W，若wnRwm，則V（B，wm）＝0，V（C，wm）＝1，且B、C相關(guān)。那么根據(jù)歸納假設(shè)有：B?wm，C∈wm，且B、C相關(guān)，因而有 B∈wm，C∈wm，且B、C相關(guān)。因為wnRwn，所以有 B∈wn，C∈wn，且B、C相關(guān)。這樣，有wn├ B，wn├C且B、C相關(guān)，那么根據(jù)公理4可以得到：wn├B→C，因為wn是強協(xié)調(diào)集，所以有（B→C）∈wn。

假設(shè)V＊（D，wn）＝0：

（1）如果存在wm∈W，wnRwm，V（B，wm）＝1，V（C，wm）＝0，根據(jù)歸納假設(shè)有：B∈wm，C?wm。假設(shè)（B→C）∈wm，則有C∈wm，矛盾。因此可得（B→C）?wm，因為wnRwm，所以wn?wm，因此（B→C）?wn。

（2）如果存在wm∈W，wnRwm，V（B，wm）＝0，V（C，wm）＝1且A、B不相關(guān)，那么根據(jù)歸納假設(shè)有：B?wm，C∈wm，且B、C不相關(guān)，因而有 B∈wm，C∈wm，且B、C不相關(guān)。這樣，有wm├ B，wm├C且B、C不相關(guān)，那么根據(jù)公理5可以得到：wm├ （B→C），因為wn是強協(xié)調(diào)集，所以有 （B→C）∈wm，因而（B→C）?wm，因為wnRwm，所以wn?wm，因此（B→C）?wn。

定理4.5 設(shè)Σ?Form（LIP），A∈Form（LIP）。

［1］如果Σ是協(xié)調(diào)的，則Σ是可滿足的；

［2］如果Σ╞IDA，則Σ├IDA；

［3］如果╞IDA，則├IDA。

證明：

［1］設(shè)Σ是協(xié)調(diào)的。則有A∈Form（LIP），使得Σ├╱IDA。由定理4.2可知，Σ能擴充為Σ1?Form（LIP），使得Σ1是強協(xié)調(diào)的并且Σ1├╱IDA，取任何B∈Σ，有B∈Σ1，由定理4.4可得V＊（B，w1）＝1，因此V＊（Σ，w1）＝1，從而Σ是可滿足的。

［2］假設(shè)Σ├╱IDA，由定理4.2可知，Σ能擴充為Σ1?Form（LIP），使得Σ1是強協(xié)調(diào)的并且Σ1├╱IDA，取任何B∈Σ，有B∈Σ1，由定理4.4可得V＊（B，w1）＝1，因此V＊（Σ，w1）＝1，但是A?Σ1，由定理4.4可得V＊（A，w1）＝0。所以Σ╞╱IDA。

［3］是［2］的特殊情形。

定理4.6 設(shè)Σ?Form（LIP），A∈Form（LIP）。

［1］Σ├ （A∧ A）

［2］├╱IDA∨ A

［3］├╱IDA→A

［4］├╱IDA∧ A→B

即在該系統(tǒng)中，不矛盾律仍然是定理，但是排中律、雙重否定消去律、司各脫法則不是定理。因此，在該系統(tǒng)中，弗協(xié)調(diào)邏輯和直覺主義邏輯的基本特征都被保留了下來。由此可見，該系統(tǒng)給出了處理矛盾問題（包括悖論問題）［11－12］的一個直覺主義方案。

［1］ 杜國平.經(jīng)典邏輯視野中的弗協(xié)調(diào)邏輯［J］.華南師范大學學報，2007（5）.

［2］ 杜國平.哲思邏輯［J］.東南大學學報：哲學社會科學版，2007（4）.

［3］ 杜國平，馬亮.哲思邏輯的判定問題［J］.安徽大學學報，2007（5）.

［4］ 杜國平.知識蘊涵邏輯系統(tǒng)［J］.邏輯學研究，2008（2）.

［5］ 杜國平，王洪光，等.知識蘊涵模態(tài)邏輯系統(tǒng)［J］.徐州師范大學學報，2008（5）.

［6］ Guoping Du，Hongguang Wang，Na Li，Liang Xu.The Completeness and Decidability of Intuitive Implication Logic System［C］／／Maozu Guo，Liang Zhao，and Lipo Wang（eds.），F(xiàn)ourth International Conference on Natural Computation，Volume 4.Jinan，Shangdong，China，18－20Oct.2008.pp.573－577.

［7］ 杜國平.知識蘊涵時態(tài)邏輯系統(tǒng)［J］.安徽大學學報，2009（5）.

［8］ Hongguang Wang，Na Li，Guoping Du.Intuitive Implication Logic System［C］／／Yixin Chen，Hepu Deng，Degan Zhang，and Yingyuan Xiao（eds.），The Sixth International Conference on Fuzzy Systems and Knowledge Discovery，Vol.2，Tianjin，China，14－16Aug.2009.pp.252－256.

［9］ Guoping Du，Xiaohua Chen，Hongguang Wang.Intuitive Implication Predicate Logic System［C］／／Da Ruan，Tianrui Li，Yang Xu，Guoqing Chen，and Etienne E Kerre（eds.），The Ninth International Conference on Fuzzy Logic and Intelligent Technologies in Nuclear Science，Vol.4，Chengdu，China，2－4Aug.2010.pp.198－203.

［10］ 杜國平.可拓策略存在性研究［J］.哈爾濱工業(yè)大學學報，2006（7）.

［11］ 杜國平.集合論—泛邏輯悖論［J］.北京航空航天大學學報，2009（3）.

B81

A

1671－511X（2012）02－0018－05

2011－01－21

國家社會科學基金項目“不協(xié)調(diào)理論的推理機制研究”（10BZX054）階段性成果。

杜國平（1965－），男，江蘇盱眙人，工學、哲學雙博士，中國社會科學院哲學研究所研究員，研究方向：邏輯學。