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

杜國平

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

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

杜國平

（中國社會科學(xué)院哲學(xué)研究所，北京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)，即排中律、雙重否定消去律等在其中不是定理；當(dāng)然，我們也希望在該系統(tǒng)中不矛盾律仍然是定理，但是司各脫法則不是定理，即弗協(xié)調(diào)邏輯的特征在該系統(tǒng)中仍然得以保持。

一、形式語言

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

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

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

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

定義1.3 （Form（LIP））A∈Form（LIP），當(dāng)且僅當(dāng)它能（有窮次）由下列規(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)，當(dāng)且僅當(dāng)

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

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

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

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

使得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，當(dāng)且僅當(dāng)V（A，w）＝1并且V（B，w）＝1；

［4］V（A∨B，w）＝1，當(dāng)且僅當(dāng)V（A，w）＝1或者V（B，w）＝1；

［5］如果對于任一w′∈W，若wRw′，當(dāng)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′，當(dāng)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)的，當(dāng)且僅當(dāng)存在公式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)的，當(dāng)且僅當(dāng)Σ滿足下列條件：

［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當(dāng)且僅當(dāng)i≤j；

對于任一原子公式B，V＊（B，wn）＝1當(dāng)且僅當(dāng)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āng)D為原子公式，則由V＊的定義可知，命題成立。

［3］當(dāng)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āng)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āng)D為B→C時。

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

（1）如果對于任一wm∈W，若wnRwm，則V（B，wm）＝V（C，wm），那么根據(jù)歸納假設(shè)有：B∈wm當(dāng)且僅當(dāng)C∈wm，因為wnRwn，所以有B∈wn當(dāng)且僅當(dāng)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］.華南師范大學(xué)學(xué)報，2007（5）.

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

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

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

［5］ 杜國平，王洪光，等.知識蘊涵模態(tài)邏輯系統(tǒng)［J］.徐州師范大學(xué)學(xué)報，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］.安徽大學(xué)學(xué)報，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è)大學(xué)學(xué)報，2006（7）.

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

B81

A

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

2011－01－21

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

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