2.3 對當關系邏輯

通過上面的分析，我們可以看出，科斯塔的弗協調邏輯中的否定關系實際上是一種特殊的下反對關系。下面我們在經典邏輯系統的基礎上直接建立刻畫各種對當關系的邏輯系統。

在直覺主義邏輯系統內，對于構造性否定算子﹁有下述兩條定理：

[1]A∧﹁A不可滿足；

[2]A∨﹁A不普遍有效。

人們通常據此認為：在直覺主義邏輯系統中，構造性否定算子﹁遵守不矛盾律而不遵守排中律。

在科斯塔的弗協調邏輯系統內，對于弗協調否定算子﹁有下述兩條定理：

[1]A∧﹁A可滿足；

[2]A∨﹁A普遍有效。

人們通常據此認為：在科斯塔的弗協調邏輯系統中，弗協調否定算子﹁遵守排中律而不遵守不矛盾律。

直覺主義邏輯和科斯塔的弗協調邏輯都是撇開經典否定算子而在正命題邏輯的基礎上直接引入新的否定算子而建立邏輯系統的。下面我們來建立對當關系邏輯系統，在經典邏輯系統基礎上構建滿足上述條件的構造性否定算子和弗協調否定算子。

對當關系邏輯的形式語言L是在經典命題邏輯形式語言的基礎上增加一元聯結符“*”而得到的。

公式的形成規則中增加下面一條規則：如果A是公式，則*A是公式。并在形式語言中增加如下兩個定義符號：

△A=def*﹁A

▽A=def﹁*A

其中，一元聯結符△稱為弗協調聯結符，一元聯結符▽稱為直覺主義聯結符。

對當關系邏輯的公理系統是在經典命題邏輯系統中增加一條公理而形成。包括如下公理模式和推理規則：

推理規則（分離規則MP）：從A和A→B可推出B。

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

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

[1]Ak是公理；

[2]Ak∈Σ；

[3]有i,j＜k，使得Ai=Aj→Ak。

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

定義2.3.2 如果公式A由?形式可推演，則稱公式A是可證明的。由?到A形式可推演的一個公式序列稱為公式A的一個證明。如果公式A是可證明的，則稱公式A為對當關系邏輯系統的定理，符號記為├A。

顯然，經典命題邏輯的定理在對當關系邏輯中依然成立。所以，在下面定理的證明中將直接使用經典命題邏輯的定理（簡記為PTh）。

在對當關系邏輯中有如下定理：

定理2.3.1 ├﹁*A→﹁A

定理2.3.2 ├﹁A→△A

定理2.3.3 ├﹁△A→A

定理2.3.4 ├A→﹁▽A

定理2.3.5 ├▽A→﹁A

定理2.3.6 ├A∧▽A→B

證明：

定理2.3.7 ├A∨△A

證明：

定理2.3.8

[1]├（A→B）→（（A→▽B）→﹁A）

[2]├（﹁A→B）→（（﹁A→▽B）→A）

[3]├（A→B）→（（A→▽B）→（A→▽A））

[4]├（▽A→B）→（（▽A→▽B）→（▽A→A））

證明：[1]、[2]、[4]略。

[3]

定義2.3.3 對當關系邏輯的一個賦值v是以所有公式的集Form（L）為定義域、以｛0,1｝ 為值域的一個函數，并滿足下列條件：

[1]v（﹁A）=1，當且僅當，v（A）=0；

[2]如果v（*A）=0，那么v（A）=0；

[3]v（A∧B）=1，當且僅當，v（A）=v（B）=1；

[4]v（A∨B）=1，當且僅當，v（A）=1或者v（B）=1；

[5]v（A→B）=1，當且僅當v（A）=0或者v（B）=1。

可以證明：

定理2.3.9 設A為任一公式，v是一對當關系邏輯賦值，則

[1]如果v（A）=0，那么v（△A）=1；

[2]如果v（A）=1，那么v（▽A）=0。

定義2.3.4 稱一對當關系邏輯賦值v為公式集Γ的模型，當且僅當，對Γ中任一公式A有v（A）=1；稱A為Γ的語義后承，記作Γ╞A，當且僅當，Γ的任一模型都使得v（A）=1; ?╞A簡記為╞A，此時對任一個賦值v都有v（A）=1，因而也稱A為有效的。

定理2.3.10 設A為任意的對當關系邏輯公式，則

[1]╞▽△A→A；

[2]╞A→△▽A；

[3]╞（A→B）→（▽B→△A）

[4]╞（A→▽B）→（B→△A）

[5]╞（△A→B）→（▽B→A）

[6]╞（△A→▽B）→（B→A）

[7]╞（A→B）→（（A→▽B）→△A）

[8]╞（△A→B）→（（△A→▽B）→A）

證明：

[1]假設╞▽△A→A不成立，則存在對當關系邏輯賦值v使得

（1）v（▽△A→A）=0

由（1）可得：

（2）v（▽△A）=1

（3）v（A）=0

由（2）可得：

（4）v（△A）=0

由（4）可得：

（5）v（A）=1

（3）、（5）矛盾。所以假設不成立。因此╞▽△A→A。

[2]、[3]、[4]、[5]、[6]略。

定理2.3.11 設A、B為任意的對當關系邏輯公式，則下列公式都不是對當關系邏輯的有效式：

[1]*A→A

[2]A→﹁△A

[3]﹁A→▽A

[4]A∧△A→B

[5]A∧*A→B

[6]A∨▽A

[7]A∨*A

[8]▽（A∧▽A）

[9]*（A∧*A）

[10]△（A∧△A）

[11]（A→B）→（（A→*B）→*A）

[12]（*A→B）→（（*A→*B）→A）

[13]（A→B）→（（A→△B）→△A）

[14]（△A→B）→（（△A→△B）→A）

[15]（A→B）→（（A→▽B）→▽A）

[16]（▽A→B）→（（▽A→▽B）→A）

定理2.3.12 對當關系邏輯的公理都是有效的。

定理2.3.13 如果Σ╞A并且Σ╞A→B，那么Σ╞B。

定理2.3.14（對當關系邏輯可靠性定理） 設Σ為任一公式集，A為任一公式，則

[1]如果Σ├A，那么Σ╞A；

[2]如果├A，那么╞A。

定義2.3.5 令Γ為一公式集，

[1]；

[2]稱Γ為協調的，當且僅當，，否則，稱Γ為不協調的；

[3]稱一協調集Γ為極大的，當且僅當，Γ是協調的，并且對任一公式A，如果A?Γ，則?！龋鸄｝是不協調的；

定理2.3.15 如果Γ是極大協調的，那么：

[1]Γ├A?A∈Γ；

[2]A∈Γ，當且僅當，﹁A?Γ；

[3]如果A∈Γ，那么*A∈Γ；

[4]如果A?Γ，那么△A∈Γ；

[5]如果A∈Γ，那么▽A?Γ；

[6]A∧B∈Γ，當且僅當，A∈Γ并且B∈Γ；

[7]A∨B∈Γ，當且僅當，A∈?；蛘連∈Γ；

[8]A→B∈Γ，當且僅當，A??；蛘連∈Γ。

證明：選證[1]、[3]、[4]、[5]，其他略。

[1]?顯然成立。

再證?。設Γ├A，但是A?Γ。因為Γ是極大協調集，所以Γ∪｛A｝├C∧﹁C。因此有：

這樣，Γ就不協調。這與Γ是極大協調集相矛盾。因此假設不成立。

[3]如果A∈Γ，那么Γ├A。又因為Γ├A→*A，所以有Γ├*A，根據本定理[1]可得：*A∈Γ。

[4]如果A?Γ，那么根據定理2.3.3和本定理[1]可得：﹁△A?Σ，再由本定理[2]可得：△A∈Σ。

[5]如果A∈Γ，那么根據定理2.3.4和本定理[1]可得：﹁▽A∈Γ，再由本定理[2]可得：▽A?Γ。

定理2.3.16 設Γ是一極大協調集，對任一公式A，令

v。（A）=1當且僅當A∈Γ。

則v。是一對當關系邏輯賦值。即v。是極大協調集Γ的模型。

定理2.3.17 任一協調的公式集Γ均可擴充為極大協調的。

定理2.3.18 任一協調的公式集Γ均有模型。

定理2.3.19（對當關系邏輯完全性定理） 設Σ為任一公式集，A為任一公式，則

[1]如果Σ╞A，那么Σ├A；

[2]如果╞A，那么├A。

證明：

[1]如果Σ╞A，則?！龋鐰｝沒有模型。所以?！龋鐰｝不協調。因此有：

[2]當Σ為?時，由[1]直接可得。

在對當關系邏輯中，對于一元聯結符﹁來說，A與﹁A之間有下列關系成立：

對于任一對當關系邏輯的賦值v，如果v（A）=1，那么v（﹁A）=0；如果v（﹁A）=0，那么v（A）=1；如果v（A）=0，那么v（﹁A）=1；如果v（﹁A）=1，那么v（A）=0。所以，A與﹁A之間是矛盾關系。

對于一元聯結符*來說，A與*A之間有下列關系成立：

對于任一對當關系邏輯的賦值v，如果v（A）=1，那么v（*A）=1；如果v（*A）=0，那么v（A）=0；如果v（A）=0，那么v（*A）=1或者v（*A）=0；如果v（*A）=1，那么v（A）=1或者v（A）=0。所以，A與*A之間是差等關系。

對于一元聯結符▽來說，A與▽A之間有下列關系成立：

對于任一對當關系邏輯的賦值v，如果v（A）=1，那么v（▽A）=0；如果v（▽A）=1，那么v（A）=0；如果v（A）=0，那么v（▽A）=1或者v（▽A）=0；如果v（▽A）=0，那么v（A）=1或者v（A）=0。所以，A與▽A之間是上反對關系。

對于一元聯結符△來說，A與△A之間有下列關系成立：

對于任一對當關系邏輯的賦值v，如果v（A）=0，那么v（△A）=1；如果v（△A）=0，那么v（A）=1；如果v（A）=1，那么v（△A）=1或者v（△A）=0；如果v（△A）=1，那么v（A）=1或者v（A）=0。所以，A與△A之間是下反對關系。

定理2.3.20

[1]A∧﹁A不可滿足；

[2]A∨﹁A有效；

[3]A∧▽A不可滿足；

[4]A∨▽A不有效；

[5]A∧△A可滿足；

[6]A∨△A有效；

[7]A∧ *A可滿足；

[8]A∨ *A不有效。

在對當關系邏輯系統中：因為A∧﹁A是沒有模型的，A∨﹁A是有效式，所以一元聯結符﹁既符合不矛盾律又符合排中律；因為A∧▽A是沒有模型的，A∨▽A不是有效式，所以一元聯結符▽符合不矛盾律但不符合排中律；因為A∧△A有模型，A∨△A是有效式，所以一元聯結符△不符合不矛盾律但符合排中律；因為A∧*A有模型，A∨*A不是有效式，所以一元聯結符*既不符合不矛盾律也不符合排中律。

一般把不矛盾律在其中不普遍有效的邏輯系統稱為弗協調邏輯系統，所以我們將一元聯結符△稱為弗協調聯結符；一般把排中律在其中不普遍有效的邏輯系統稱為直覺主義邏輯系統，所以我們將一元聯結符▽稱為直覺主義聯結符；一元聯結符*既不符合不矛盾律也不符合排中律，所以可以說，*既是弗協調聯結符也是直覺主義聯結符。因此，對當關系邏輯可以作為不協調理論和直覺主義理論的邏輯工具。

因為A∧△A→B和A∧*A→B均不是對當關系邏輯系統中的有效式，所以著名的司各脫法則對于一元聯結符△和*均不成立。