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∉Γ，则Γ∪｛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∈Γ或者B∈Γ；

[8]A→B∈Γ，当且仅当，A∉Γ或者B∈Γ。

证明：选证[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，则Γ∪｛﹁A｝没有模型。所以Γ∪｛﹁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均不是对当关系逻辑系统中的有效式，所以著名的司各脱法则对于一元联结符△和*均不成立。