杜國平

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

本文擬基于括號表示法[1-4]以二元聯(lián)結(jié)詞“合舍”作為唯一初始聯(lián)結(jié)詞，建立一個命題邏輯自然推演系統(tǒng)；嚴格給出關(guān)涉定理證明的“化歸”定義，進而探討定理機械證明的能行性步驟。

一、形式語言

定義1 形式語言LDP包括如下兩類符號：

(1)命題符號：p1，p2，…，pn，pn+1，…；

(2)聯(lián)結(jié)詞符號：「，」。

形式語言LDP中初始聯(lián)結(jié)詞只有一對左右括號“「」”。

定義2 形式語言LDP中的公式當且僅當有限次使用如下規(guī)則而得：

(1)單獨的一個命題符號是公式；

(2)若符號串F、G是公式，則「FG」是公式。

通常以大寫字母A、B、C等表示任意的公式。LDP中所有公式的集合記為Form(LDP)。

聯(lián)結(jié)詞「FG」的語義可用真值表直觀表示如下(表1)：

表1 聯(lián)結(jié)詞「FG」語義真值表

由此可見，「FG」就是F、G的合舍[5]。為了表達方便，定義引入如下一些縮寫符號：

定義3

(A)=def「AA」

[AB]=def「「AA」「BB」」

=def「「AB」「AB」」

『AB』=def(「(A)B)」)=def「「「AA」B」「「AA」B」」

命題1 聯(lián)結(jié)詞“「」”對于二值真值函數(shù)其表達能力是足夠的。

二、公理系統(tǒng)

以合舍作為初始聯(lián)結(jié)詞的命題邏輯自然推演系統(tǒng)NPD1包括如下5條推理規(guī)則：

規(guī)則D1D├D。簡記為Ref。

規(guī)則D2 如果Σ├D，那么Σ,Σ′├D。簡記為+。

規(guī)則D3 如果∑，A├B，且Σ├「BB」，那么Σ├「AB」。簡記為「」+。

規(guī)則D4 如果Σ，「CC」├「AB」，并且Σ，「CC」├A，那么Σ├C。簡記為「」l-。

規(guī)則D5 如果Σ，C├「AB」，并且Σ，C├B，那么Σ├「CC」。簡記為「」r-。

規(guī)則D1、規(guī)則D2是通常的命題邏輯自然推理規(guī)則。規(guī)則D3、規(guī)則D4和規(guī)則D5這3條規(guī)則是關(guān)于唯一聯(lián)結(jié)詞括號“「」”的特征推理規(guī)則，其中規(guī)則D3是括號“「」”的引入規(guī)則，規(guī)則D4、規(guī)則D5是括號“「」”的消去規(guī)則，規(guī)則D4是括號左消去規(guī)則，規(guī)則D5是括號右消去規(guī)則。

三、只含初始聯(lián)結(jié)詞“「」”定理的推演

定義4 公式A在系統(tǒng)NP1中由公式集Σ形式可推演，記為Σ├A，當且僅當Σ├A能由有限次使用規(guī)則SR1～規(guī)則SR5而生成。

引理1 若A∈Σ，則Σ├A。

該引理簡記為∈。

引理2 若Σ├Σ′，且Σ′├C，則Σ├C。

該引理簡記為?。

定理1 若Σ├A，且Σ├「AB」，則Σ├C。

證明：

1.Σ├A前提

2.Σ├「AB」 前提

3.Σ，「CC」├A1， +

4.Σ，「CC」├「AB」 2， +

5.Σ├C3，4，「」l-

對于定理1，特別地有：若Σ├A，且Σ├「AA」，則Σ├B。

定理2 若Σ，A├「CC」，且Σ，B├「CC」，則Σ，C├「AB」。

證明：

1.Σ，A├「CC」 前提

2.Σ，B├「CC」 前提

3.Σ，C，B├「CC」 2，+

4.Σ,C，B├C∈

5.Σ，C├「BB」 3，4，「」r-

6.Σ，C，A├「CC」 1，+

7.Σ，C，A├C∈

8.Σ，C，A├B6，7，定理1

9.Σ，C├「AB」 5，8，「」+

定理3 若Σ├「AA」，并且Σ├「BB」，則Σ├「AB」。

定理4 若Σ├「「AA」B」，則Σ├A。

證明：

1.Σ├「「AA」B」 前提

2.Σ，「AA」├「AA」 ∈

3.Σ，「AA」├「「AA」B」 1，+

4.Σ├A2，3，「」l-

定理5 若Σ├「AB」，則Σ├「BB」。

四、若干定義聯(lián)結(jié)詞“「」”定理的推演

定理6 若Σ├「「AA」「AA」」，則Σ├A。

證明：

1.Σ├「「AA」」 前提

2.Σ，「AA」├「「AA」「AA」」 1，+

3.Σ，「AA」├「AA」 ∈

4.Σ├A2，3，「」l-

根據(jù)定義3，該定理可以簡記為：Σ├((A))，則Σ├A。

定理7 若Σ├A，則Σ├「「AA」「AA」」。

根據(jù)定義3，該定理可以簡記為：Σ├A，則Σ├((A))。

定理8 若Σ├「AB」，則Σ├「BA」。

證明：

1.Σ├「AB」 前提

2.Σ，「「AA」「AA」」├「AB」 1，+

3.Σ，「「AA」「AA」」├「「AA」「AA」」 ∈

4.Σ，「「AA」「AA」」├A3，定理6

5.Σ├「AA」 2，4，「」l-

6.Σ，B，「AA」├「AB」 1，+

7.Σ├，B，「AA」├B∈

8.Σ├，B├「「AA」「AA」」 6，7，「」r-

9.Σ├，B├A7，8，定理6

10.Σ├「BA」 5，9，「」+

對于定理8，特別地有：若Σ├「「AA」「BB」」，則Σ├「「BB」「AA」」。根據(jù)定義3，這可以簡記為：若Σ├[AB]，則Σ├[BA]。

定理9 若Σ├「「AB」「AB」」，則Σ├「「BA」「BA」」。

證明：

1.Σ├「「AB」「AB」」 前提

2.Σ，「BA」├「BA」 ∈

3.Σ，「BA」├「AB」 2，定理8

4.Σ，「BA」├「「AB」「AB」」 1，+

5.Σ├「「BA」「BA」」 3，4，「」r-

根據(jù)定義3，該定理可以簡記為：Σ├，則Σ├。

定理10 若Σ├「「「「AB」「AB」」C」「「「AB」「AB」」C」」，則Σ├「「A「「BC」「BC」」」「A「「BC」「BC」」」」。

根據(jù)定義3，該定理可以簡記為：Σ├<C>，則Σ├>。

以下，我們將<C>按照左結(jié)合順序簡記為；類似地，將[[AB]C]按照左結(jié)合順序簡記為[ABC]。

定理11 若Σ├A，則Σ├「「AB」「AB」」。

根據(jù)定義3，該定理可以簡記為：Σ├A，則Σ├。

定理12

(1) 若Σ，「CC」├「AA」，則├，A├C；

(2) 若Σ，A├C，則Σ，「CC」├「AA」；

(3) 若Σ，A├「CC」，則Σ，C├「AA」；

(4) 若Σ，「AA」├C，則Σ，「CC」├A。

證明：

(1)

1.Σ，「CC」├「AA」 前提

2.Σ，A，「CC」├「AA」 1，+

3.Σ，A，「CC」├A∈

4.Σ，A├C3，4，「」l-

(2)(3)(4)類似可證。

根據(jù)定義3，該定理可以簡記為：

(1) 若Σ，(C)├(A)，則Σ，A├C；

(2) 若Σ，A├C，則Σ，(C)├(A)；

(3) 若Σ，A├(C)，則Σ，C├(A)；

(4) 若Σ，(A)├C，則Σ，(C)├A。

定理13 若Σ,A├C，并且Σ，B├C，則Σ，「「AB」「AB」」├C。

根據(jù)定義3，該定理可以簡記為：若Σ，A├C，并且Σ，B├C，則Σ，├C。

定理14

(1) 若Σ├A，則Σ├「「AB」「AB」」；

(2) 若Σ├B，則(Σ├「「AB」「AB」」。

根據(jù)定義3，該定理可以簡記為：

(1) 若Σ├A，則Σ├；

(2) 若Σ├B，則Σ├。

定理15 若Σ├A，且Σ├B，則Σ├「「AA」「BB」」。

證明：

1.Σ├A前提

2.Σ├B前提

3.Σ├「「AA」「AA」」 1，定理7

4.Σ├「「BB」「BB」」 2，定理7

5.Σ├「「AA」「BB」」 3，4，定理3

根據(jù)定義3，該定理可以簡記為：若Σ├A，且Σ├B，則Σ├[AB]。

定理16 若Σ├「「AA」「BC」」，則Σ├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」。

證明：

1.Σ├「「AA」「BC」」 前提

2.Σ├A1，定理3

3.Σ├「「BC」「BC」」 1，定理5

4.Σ，A，B├「「AA」「BB」」 定理15

5.Σ，A，B├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」 4，定理14

6.Σ，A，C├「「AA」「CC」」 定理15

7.Σ，A，C├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」 6，定理14

8.Σ，A，「「BC」「BC」」├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」

5，7，定理13

9.Σ├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」 2，3，8，引理2

根據(jù)定義3，該定理可以簡記為：Σ├[A]，則Σ├<[AB][AC]>。

定理17 若Σ├「「「「AA」「BB」」「「AA」「CC」」」「「「AA」「BB」」「「AA」「CC」」」」，則Σ├「「AA」「BC」」。

根據(jù)定義3，該定理可以簡記為：Σ├<[AB][AC]>，則Σ├[A]。

定理18 若Σ├「「AB」「AB」」，則Σ├「「A「「「AA」「AA」」「BB」」」「A「「「AA」「AA」」「BB」」」」。

根據(jù)定義3，該定理可以簡記為：若Σ├，則Σ├。

定理19 若Σ├「「A「「「AA」「AA」」「BB」」」「A「「「AA」「AA」」「BB」」」」，則Σ├「「AB」「AB」」。

根據(jù)定義3，該定理可以簡記為：若Σ├，則Σ├。

定理20 若Σ├「「「AA」B」「「AA」B」」，則Σ├「「「AA」「「AA」「BB」」」「「AA」「「AA」「BB」」」」。

根據(jù)定義3，該定理可以簡記為：若Σ├<(A)B>，則Σ├<(A)[AB]>。

定理21 若Σ├「「「AA」「「AA」「BB」」」「「AA」「「AA」「BB」」」」，則Σ├「「「AA」B」「「AA」B」」。

根據(jù)定義3，該定理可以簡記為：若Σ├<(A)[AB]>，則Σ├<(A)B>。

定理22 若Σ├A，則Σ├「「A「「AA」「BB」」」「A「「AA」「BB」」」」。

根據(jù)定義3，該定理可以簡記為：若Σ├A，則Σ├。

定理23 若Σ├「「A「「AA」「BB」」」「A「「AA」「BB」」」」，則Σ├A。

根據(jù)定義3，該定理可以簡記為：若Σ├，則Σ├A。

定理24Σ├「「A「AA」」「A「AA」」」。

根據(jù)定義3，該定理可以簡記為：Σ├。

定理25 若Σ├「「A「AA」」「A「AA」」」，則Σ├「「「「A「AA」」「A「AA」」」B」「「「A「AA」」「A「AA」」」B」」。

根據(jù)定義3，該定理可以簡記為：若Σ├，則Σ├<B>。

定理26 若Σ├「「「「A「AA」」「A「AA」」」B」「「「A「AA」」「A「AA」」」B」」，則Σ├「「A「AA」」「A「AA」」」。

根據(jù)定義3，該定理可以簡記為：若Σ├<B>，則Σ├。

定理27 若Σ├A，且Σ├「「「AA」B」「「AA」B」」，則Σ├B。

根據(jù)定義3，該定理可以簡記為：Σ├A，且Σ├『AB』，則Σ├B。

定理28 若Σ，A├B，則Σ├「「「AA」B」「「AA」B」」。

根據(jù)定義3，該定理可以簡記為：若Σ，A├B，則Σ├『AB』。

根據(jù)推理規(guī)則D1、推理規(guī)則D2、推理規(guī)則D4、定理27和定理28可知，系統(tǒng)NP1與通常的經(jīng)典命題邏輯系統(tǒng)等價[6]。

根據(jù)定義3，公式「「「AA」「BB」」「「AA」「BB」」」既可以簡寫為([AB])，也可以簡寫為<(A)(B)>；公式「「「AB」「AB」」「「AB」「AB」」」既可以簡寫為()，也可以簡寫為[(A)(B)]。

因此，有：

定理29

(1) 若Σ├([AB])，則Σ├<(A)(B)>；

(2) 若Σ├<(A)(B)>，則Σ├([AB])；

(3)若Σ├()，則Σ├[(A)(B)]；

(4) 若Σ├[(A)(B)]，則Σ├()。

定理30

(1) 若Σ├「AB」，則Σ├[(A)(B)]；

(2) 若Σ├[(A)(B)]，則Σ├「AB」。

定理31 令R{A}為任一包含A作為子公式的公式，R{B}為R中將所有A的出現(xiàn)替換為B而得的公式，則：

(1)Σ├R{「AB」}，當且僅當Σ├R{[(A)(B)]}；

(2)Σ├R{『AB』}，當且僅當Σ├R{(「(A)B)」)}；

(3)Σ├R{((A))}，當且僅當Σ├R{A}。

五、公式的化歸

受亞里士多德在三段論證明中所使用的化歸思想的啟發(fā)[7]，我們可以將系統(tǒng)NP1中定理的證明通過化歸來實現(xiàn)。

定義5 系統(tǒng)NP1中的化歸規(guī)則僅包括如下7條：

顯然，前述定義和定理保證了上述化歸規(guī)則的合理性。

對于包含初始聯(lián)結(jié)詞“「」”和定義聯(lián)結(jié)詞“( )”“[ ]”“< >”和“「」”的任一公式K0，如果它是系統(tǒng)NP1中的定理，可以按照如下程序綱要將其化歸為。

1．如果K0中含有符號“「」”和“「」”，使用規(guī)則R1將其中化歸為一不含符號“「」”和“「」”的公式K1；

2．反復使用規(guī)則R2將K1化歸為公式K2，使得“( )”只作用于原子公式或者原子公式前只含有若干個符號“( )”的公式之前；

3．反復使用規(guī)則R3將K2化歸為公式K3，使得K3中原子公式之前的符號“( )”至多只含有一個；

4．反復使用規(guī)則R4將K3化歸為公式K4，使得K4中符號“[ ]”符號只作用于若干原子公式或者只帶有一個符號“( )”的原子公式；

5．反復使用規(guī)則R5將K4化歸為公式K5，使得K5中符號“< >”之間的公式按照字母序和是否含有符號“( )”的順序進行排列；

6．反復使用規(guī)則R6將K5化歸為公式K6；

7．重復步驟5；

8．反復使用規(guī)則R7將K6化歸為一型公式。

例如對于公式『]>』，可根據(jù)上述程序依次將其化歸為：

第1步：

(「()]>」)

([(())(]>)])

第2步：

<[(((A)))(((B)))]<((B))[(((B)))<((C))((A))>]>>

第3步：

<[(A)(B)]]>>

第4步：

<[(A)(B)]>>

第5步：

<[A(B)][(A)(B)]B[(B)C]>

第6步：

<(B)BC>

第7步：

第8步：

因此，上述化歸程序?qū)嶋H上為NP1中定理(上述已經(jīng)證明的定理除外)的機械證明提供了一個能行性的方法。

不難發(fā)現(xiàn)，上述化歸程序不僅提供了定理的機械證明程序，而且對于任意一個公式C，如果C能被化歸為一個形如的公式，則C是系統(tǒng)NP1的定理，如果C不能被化歸為一個形如的公式，則C不是系統(tǒng)NP1的定理。特別地，如果C被化歸為一個形如[AB(B)D]的公式，則C是矛盾式。