2.4 對當(dāng)關(guān)系邏輯的判定問題

下面我們證明對當(dāng)關(guān)系邏輯的判定定理，并給出幾種判定程序。

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的復(fù)雜度指的是A中所含聯(lián)結(jié)詞的數(shù)目。

定義2.4.3 公式A的分支真值表指的是按照下述步驟構(gòu)造出來的反映A的可能真值情況的圖表。

構(gòu)造公式A的分支真值表主要包括以下兩個(gè)步驟：

第一步 列出A中出現(xiàn)的所有命題符，并列出這些命題符的各種真值組合。例如，假如公式A中只有兩個(gè)命題符p0和p1，那么它們的真值組合情形如下：

第二步 按照子公式的復(fù)雜度由小到大依次列出公式A的所有子公式（相同復(fù)雜度的子公式按照字母序或者下標(biāo)序排列），并按照下述規(guī)則列出它們的值：

[1]對于聯(lián)結(jié)詞﹁、→、∧和∨，計(jì)算方法和經(jīng)典真值表一樣；

[2]子公式形如*B，如果B的值為1，則*B在該行的值為1；如果B的值為0，則將該行分裂為兩行，其中第一行*B的值為1，第二行*B的值為0。

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

根據(jù)對當(dāng)關(guān)系邏輯的定義，公式A就是（p1→▽p2）→（p2→△p1）。

定理2.4.1 對當(dāng)關(guān)系邏輯是可判定的。

證明：

[1]設(shè)A是任一對當(dāng)關(guān)系邏輯公式，v是任一對當(dāng)關(guān)系邏輯賦值。令

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

給定公式A的一個(gè)分支真值表Q，對于Q中的第k（k≥2）行，有一個(gè)映射Qk：

Subform（A）→｛0,1｝

使得當(dāng)B∈Subform（A）時(shí)，Qk（B）等于B在第k行的值。

可以證明，對于任一賦值v，總存在一個(gè)Qk,Qk=vA。

[2]對于任一Qk，我們可以按照下面的方式將它擴(kuò)張成一個(gè)從Form（L）到｛0,1｝的映射：

對于任一對當(dāng)關(guān)系邏輯公式B，

（1）當(dāng)B∈Subform（A）時(shí)，；

（2）當(dāng)B?Subform（A）時(shí)，

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

②如果B=*C，那么當(dāng)且僅當(dāng)。容易驗(yàn)證，映射具有下述性質(zhì)：

（1）；

（2）；

（3）或者；

（4）并且 ；

（5）或者。

可以證明是一個(gè)對當(dāng)關(guān)系邏輯賦值，并且 。

[3]當(dāng)分支真值表Q中最后一列只含有1時(shí)，根據(jù)[1]可知，任一賦值v到Subform（A）上的限制vA都等于某個(gè)Qk,v（A）=vA（A）=Qk（A）=1。因此，A在任一賦值下的值都是1，即A是有效式，根據(jù)對當(dāng)關(guān)系邏輯的完全性定理可知A是對當(dāng)關(guān)系邏輯的定理。

當(dāng)A為對當(dāng)關(guān)系邏輯的定理時(shí)，根據(jù)對當(dāng)關(guān)系邏輯的可靠性定理可知，A在任一對當(dāng)關(guān)系邏輯賦值下的值都是1，當(dāng)然對各個(gè)也有，從而有。所以在Q中最后一列只含有1。

所以，一對當(dāng)關(guān)系邏輯公式A是對當(dāng)關(guān)系邏輯的定理，當(dāng)且僅當(dāng)，A的分支真值表Q中最后一列只含有1。即分支真值表是一個(gè)判定任一對當(dāng)關(guān)系邏輯公式是否是對當(dāng)關(guān)系邏輯定理的判定程序。

2.4.2 分支歸謬賦值法

分支歸謬賦值法的基本思想和經(jīng)典的歸謬賦值法是基本一致的：為了判定任一對當(dāng)關(guān)系邏輯公式A是否是有效式，先假設(shè)A不是有效式，那么由此可以斷定存在一個(gè)對當(dāng)關(guān)系邏輯賦值v使得A假。根據(jù)對當(dāng)關(guān)系邏輯的賦值定義，我們可以求出公式A中每個(gè)子公式的賦值。如果在這個(gè)賦值中，必須給同一子公式既賦值為真，又賦值為假，即出現(xiàn)矛盾，那么說明假設(shè)不成立，由此我們可以斷定公式A是有效式；如果在這個(gè)賦值中，沒有出現(xiàn)矛盾，也就是說找到了一個(gè)對當(dāng)關(guān)系邏輯賦值，使得A假，那么由此我們可以斷定公式A不是有效式。

分支歸謬賦值法的基本思想和經(jīng)典的歸謬賦值法的不同之處在于：如果遇到v（A）=0，那么求v（*A）的值時(shí)將分為兩種情況來考慮，一種是讓v（*A）=1，一種是讓v（*A）=0；如果遇到v（*A）=1，那么求v（A）的值時(shí)也將分為兩種情況來考慮，一種是讓v（A）=1，一種是讓v（A）=0。

例如：用分支歸謬賦值法判定（*﹁A→B）→（（*﹁A→﹁*B）→A）是否是有效式。

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

再如：用分支歸謬賦值法判定（﹁A→﹁B）→（（﹁A→*B）→A）是否是有效式。

盡管在第二個(gè)分支表中出現(xiàn)了矛盾，但是因?yàn)樵诘谝粋€(gè)分支表中沒有出現(xiàn)矛盾，所以可以判定（﹁A→﹁B）→（（﹁A→*B）→A）不是有效式。

2.4.3 分支樹圖方法

分支樹圖方法和經(jīng)典命題邏輯的樹圖方法基本相同。它包括如下九條規(guī)則：

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

因?yàn)槲ㄒ坏囊粋€(gè)分枝封閉，所以﹁* *﹁A→A是有效式。

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

由分枝樹圖可以看出，在六個(gè)分枝中，只有一個(gè)分枝封閉，其它五個(gè)分枝都沒有封閉，所以（*A→B）（（*A→*B）→A）不是有效式。