2.4 对当关系逻辑的判定问题

下面我们证明对当关系逻辑的判定定理，并给出几种判定程序。

2.4.1 分支真值表

定义2.4.1 Subform（A）称为公式A的子公式集。

[1]如果A∈Atom（L），则Subform（A）=｛A｝；

[2]如果A=（⊙B），则Subform（A）=Subform（B）∪｛（⊙B）｝；

[3]如果A=，则

Subform（A）=Subform（B）∪Subform（C）∪｛｝。

其中⊙B指的是﹁B或*B,指的是B→C、B∧C或B∨C。

如果 B∈Subform（A），则称B为A的子公式。

定义2.4.2 公式A的复杂度指的是A中所含联结词的数目。

定义2.4.3 公式A的分支真值表指的是按照下述步骤构造出来的反映A的可能真值情况的图表。

构造公式A的分支真值表主要包括以下两个步骤：

第一步 列出A中出现的所有命题符，并列出这些命题符的各种真值组合。例如，假如公式A中只有两个命题符p0和p1，那么它们的真值组合情形如下：

第二步 按照子公式的复杂度由小到大依次列出公式A的所有子公式（相同复杂度的子公式按照字母序或者下标序排列），并按照下述规则列出它们的值：

[1]对于联结词﹁、→、∧和∨，计算方法和经典真值表一样；

[2]子公式形如*B，如果B的值为1，则*B在该行的值为1；如果B的值为0，则将该行分裂为两行，其中第一行*B的值为1，第二行*B的值为0。

例如公式A:（p1→﹁*p2）→（p2→*﹁p1）的分支真值表为：

根据对当关系逻辑的定义，公式A就是（p1→▽p2）→（p2→△p1）。

定理2.4.1 对当关系逻辑是可判定的。

证明：

[1]设A是任一对当关系逻辑公式，v是任一对当关系逻辑赋值。令

那么有：对于任一公式B∈Subform（A）,vA（B）=v（B），特别地，vA（A）=v（A）。

给定公式A的一个分支真值表Q，对于Q中的第k（k≥2）行，有一个映射Qk：

Subform（A）→｛0,1｝

使得当B∈Subform（A）时，Qk（B）等于B在第k行的值。

可以证明，对于任一赋值v，总存在一个Qk,Qk=vA。

[2]对于任一Qk，我们可以按照下面的方式将它扩张成一个从Form（L）到｛0,1｝的映射：

对于任一对当关系逻辑公式B，

（1）当B∈Subform（A）时，；

（2）当B∉Subform（A）时，

①如果B∈Atom（L），那么；

②如果B=*C，那么当且仅当。容易验证，映射具有下述性质：

（1）；

（2）；

（3）或者；

（4）并且 ；

（5）或者。

可以证明是一个对当关系逻辑赋值，并且 。

[3]当分支真值表Q中最后一列只含有1时，根据[1]可知，任一赋值v到Subform（A）上的限制vA都等于某个Qk,v（A）=vA（A）=Qk（A）=1。因此，A在任一赋值下的值都是1，即A是有效式，根据对当关系逻辑的完全性定理可知A是对当关系逻辑的定理。

当A为对当关系逻辑的定理时，根据对当关系逻辑的可靠性定理可知，A在任一对当关系逻辑赋值下的值都是1，当然对各个也有，从而有。所以在Q中最后一列只含有1。

所以，一对当关系逻辑公式A是对当关系逻辑的定理，当且仅当，A的分支真值表Q中最后一列只含有1。即分支真值表是一个判定任一对当关系逻辑公式是否是对当关系逻辑定理的判定程序。

2.4.2 分支归谬赋值法

分支归谬赋值法的基本思想和经典的归谬赋值法是基本一致的：为了判定任一对当关系逻辑公式A是否是有效式，先假设A不是有效式，那么由此可以断定存在一个对当关系逻辑赋值v使得A假。根据对当关系逻辑的赋值定义，我们可以求出公式A中每个子公式的赋值。如果在这个赋值中，必须给同一子公式既赋值为真，又赋值为假，即出现矛盾，那么说明假设不成立，由此我们可以断定公式A是有效式；如果在这个赋值中，没有出现矛盾，也就是说找到了一个对当关系逻辑赋值，使得A假，那么由此我们可以断定公式A不是有效式。

分支归谬赋值法的基本思想和经典的归谬赋值法的不同之处在于：如果遇到v（A）=0，那么求v（*A）的值时将分为两种情况来考虑，一种是让v（*A）=1，一种是让v（*A）=0；如果遇到v（*A）=1，那么求v（A）的值时也将分为两种情况来考虑，一种是让v（A）=1，一种是让v（A）=0。

例如：用分支归谬赋值法判定（*﹁A→B）→（（*﹁A→﹁*B）→A）是否是有效式。

（3）和（9）矛盾，因此（*﹁A→B）→（（*﹁A→﹁*B）→A）是有效式。

再如：用分支归谬赋值法判定（﹁A→﹁B）→（（﹁A→*B）→A）是否是有效式。

尽管在第二个分支表中出现了矛盾，但是因为在第一个分支表中没有出现矛盾，所以可以判定（﹁A→﹁B）→（（﹁A→*B）→A）不是有效式。

2.4.3 分支树图方法

分支树图方法和经典命题逻辑的树图方法基本相同。它包括如下九条规则：

例如：用分支树图方法判定﹁**﹁A→A是否是有效式。

因为唯一的一个分枝封闭，所以﹁* *﹁A→A是有效式。

再如：用分支树图方法判定（*A→B）（（*A→*B）→A）是否是有效式。

由分枝树图可以看出，在六个分枝中，只有一个分枝封闭，其它五个分枝都没有封闭，所以（*A→B）（（*A→*B）→A）不是有效式。