杜國(guó)平

(1.中國(guó)社會(huì)科學(xué)院大學(xué) 哲學(xué)院， 北京 102488； 2.中國(guó)社會(huì)科學(xué)院 哲學(xué)研究所， 北京 100732)

經(jīng)典命題邏輯有多種不同的公理系統(tǒng)，其中以否定和蘊(yùn)涵作為初始聯(lián)結(jié)詞的公理系統(tǒng)使用最為廣泛。對(duì)于這類公理系統(tǒng)中定理的能行證明是邏輯基礎(chǔ)理論研究的一個(gè)重要課題，近期國(guó)內(nèi)學(xué)者秦一男[1]、李晟[2]、程和祥[3-4]等都對(duì)此進(jìn)行了深入探討。受亞里士多德化歸思想的啟發(fā)，本文從這一視角對(duì)相關(guān)問題展開進(jìn)一步探討，給出一種新的公理系統(tǒng)定理證明的能行方法。

一、基元、基式

本文以如下公理系統(tǒng)L但不限于這一系統(tǒng)作為討論的標(biāo)的之一。該系統(tǒng)包含如下3條公理和1條推理規(guī)則：

Ax1 (B→(C→B))

Ax2 ((B→(C→D))→((B→C)→(B→D)))

Ax3 (((C)→(B))→(((C)→B)→C))

推理規(guī)則：由B和(B→C)可得出C[5]。

為了縮短公式顯示長(zhǎng)度和表達(dá)方便，下面使用在系列論文中闡述構(gòu)建的括號(hào)表示法將上述公理系統(tǒng)重新表達(dá)[6-11]。借用括號(hào)表示法的思想，在本文的形式語言中，初始聯(lián)接詞符號(hào)只有一對(duì)左右括號(hào)〈 〉，兩個(gè)常用的聯(lián)接詞符號(hào)“否定”和“蘊(yùn)涵”通過以下定義引入：

(A) =def〈AA〉

[AB] =def〈A〈BB〉〉

據(jù)此，公理系統(tǒng)L的3條公理和1條推理規(guī)則可簡(jiǎn)化表述為：

Ax1 [B[CB]]

Ax2 [[B[CD]][[BC][BD]]]

Ax3 [[(C)(B)][[(C)B]C]]

推理規(guī)則：由B和[BC]可得出C。簡(jiǎn)記為MP。

如上所示，本文之所以使用括號(hào)表示法，一方面使用括號(hào)表示法可以精簡(jiǎn)公式，另一方面通過定義引入其他括號(hào)，既實(shí)現(xiàn)了對(duì)不同聯(lián)接詞靈活的表達(dá)，同時(shí)也不影響直觀閱讀[12]。

定義1.1任一大寫字母A、B、C等稱為基元。

定義1.2若X、Y是基元，則X、(X)稱為單基式；[XY]、[X(Y)]、[(X)Y]、[(X)(Y)]、([XY])、([X(Y)])、([(X)Y])、([(X)(Y)])、[[X(Y)]([(X)Y])]和[[XY]([(X)(Y)])]稱為雙基式。單基式和雙基式合稱基式。

定義1.3對(duì)于形如[X1[X2…[XnY]…]]的公式，稱X1、X2、…、Xn為其若干前件，稱Y為其后件。

二、定理能行證明化歸主程序

亞里士多德在其構(gòu)建的三段論系統(tǒng)中，對(duì)作為公理之外的其他三段論形式有效性的證明采用了化歸的方法，即將需要證明其有效性的三段論形式通過嚴(yán)格的能保持有效性的變形規(guī)則，逐步將其化歸為作為公理的三段論形式[13]。受此啟發(fā)，下面我們首先給出公理系統(tǒng)L任一定理證明的化歸主程序。

下文中，以大寫斜體字母X、Y、Z、M、N等以及R表述任一公式；以R{X}表述一個(gè)含有X作為子公式的公式R。

定義2.1對(duì)于主程序中的規(guī)則：

RX RY 規(guī)則0.01

R{X}稱為規(guī)則0.01的輸入，R{Y}稱為規(guī)則0.01的輸出；X稱為輸入的對(duì)象，Y稱為輸出的目標(biāo)。

(一)雙否消去、否定內(nèi)移規(guī)則

1.雙否消去規(guī)則

R((X)) RX 規(guī)則1.11

將公式R中形如((X))的公式替換為X。

2.否定內(nèi)移規(guī)則

R ([X([YZ])]) R [[XY]([X(Z)])] 規(guī)則1.21

R ([[XY]Z]) R[[(X)Z]([YZ])] 規(guī)則1.22

理論上，還可能存在公式形如([X[YZ]])以及([([XY])Z])中的否定內(nèi)移問題。但是因?yàn)椋?1)單獨(dú)的公式([X[YZ]])以及([([XY])Z])均不是有效式(因?yàn)槿绻?[X[YZ]])以及([([XY])Z])是有效式，則([p[qr]])以及([([pq])r])也是有效式，而這是不可能的，如若pv=qv=rv=1，則([p[qr]])v=([([pq])r])v=0)，因此([X[YZ]])以及([([XY])Z])也不是定理；(2)([X[YZ]])以及([([XY])Z])沒有比其更簡(jiǎn)單的單一公式形式。因此，對(duì)于形如([X[YZ]])以及([([XY])Z])的公式，其中的否定內(nèi)移比較復(fù)雜。需要考慮其分別作為一個(gè)蘊(yùn)涵式的前、后件的情況。

R[([X[YZ]])M] R [(M)[X[YZ]]] 規(guī)則1.23

R[M([([XY])Z])] R[MX] R[MY] R[M(Z)] 規(guī)則1.24

[([([XY])Z])M] R[(M)[([XY])Z]] 規(guī)則1.25

R[M([X[YZ]])] R[MX] R[M(Y)] R[M(Z)] 規(guī)則1.26

任一公式經(jīng)過對(duì)其反復(fù)使用雙否消去規(guī)則、否定內(nèi)移規(guī)則之后，不難發(fā)現(xiàn)，該公式被化歸為若干個(gè)基式或者若干個(gè)其若干前件和后件均為基式的蘊(yùn)涵式，簡(jiǎn)稱為基蘊(yùn)涵式。

(二)移動(dòng)、排序規(guī)則

R[(Y)(X)] R[XY] 規(guī)則2.11

R[Y(X)] R[X(Y)] 規(guī)則2.12

R[(Y)X] R[(X)Y] 規(guī)則2.13

R[YX] R[(X)(Y)] 規(guī)則2.14

R[Y[XZ]] R[X[YZ]] 規(guī)則2.21

通過對(duì)反復(fù)使用雙否消去規(guī)則、否定內(nèi)移規(guī)則得到的公式再反復(fù)使用移動(dòng)、排序規(guī)則可實(shí)現(xiàn)將其化歸為將單基式移至雙基式的左邊，并按照字母序、肯定和否定序排列的公式。

(三)合并規(guī)則

R[X([XY])] R[X(Y)] 規(guī)則3.11

R[(X)([XY])] RX 規(guī)則3.12

R[[XY]([(X)Y])] R(Y) 規(guī)則3.21

R[[XY]([X(Y)])] RX 規(guī)則3.22

R[[X(Y)]([XY])] RX 規(guī)則3.23

R[[XY][X(Y)]] R[X(Y)] 規(guī)則3.31

R[[XY][(X)Y]] R[(X)Y] 規(guī)則3.32

R[X[Y[YZ]]] R[X[YZ]] 規(guī)則3.41

通過對(duì)反復(fù)使用雙否消去規(guī)則、否定內(nèi)移規(guī)則、移動(dòng)、排序規(guī)則得到的公式再反復(fù)使用合并規(guī)則可實(shí)現(xiàn)將其化歸為若干個(gè)經(jīng)過簡(jiǎn)化的基式或者若干個(gè)其若干前件和后件均為基式的蘊(yùn)涵式。

(四)歸約規(guī)則

[X[Y[(Y)Z]]][YY]規(guī)則4.11

[X[YY]][YY]規(guī)則4.12

通過歸約規(guī)則，可以將經(jīng)過前述程序處理得到的公式，進(jìn)一步化歸為[YY]。

上述主程序中的化歸規(guī)則并非都是必須的，有些可以通過其他化歸規(guī)則來實(shí)現(xiàn)，如規(guī)則3.23可通過規(guī)則2.12和規(guī)則3.22來實(shí)現(xiàn)；之所以保留這些非必須的規(guī)則是為了簡(jiǎn)化化歸步驟。

三、子程序

上述主程序給出了將任一公式化歸為形如[YY]公式的綱要，對(duì)于其中每一個(gè)規(guī)則給出的每一步程序的具體實(shí)現(xiàn)還需要更加精細(xì)的子程序以實(shí)現(xiàn)其由公理和推理規(guī)則證明定理的具體步驟。下面不一一給出細(xì)節(jié)，只例示其中的若干子程序。

子程序5.01 ├[YY]。

證明：

1 [[Y[[XY]Y]][[Y[XY]][YY]]]Ax2

2 [Y[[XY]Y]] Ax1

3 [[Y[XY]][YY]] 1、2，MP

4 [Y[XY]] Ax1

5 [YY] 3、4，MP

子程序4.12 若├[YY]，則├[X[YY]]。

證明：

1 [YY] 子程序1.11

2 [[YY][X[YY]]] Ax1

3 [X[YY]] 1、2，MP

子程序2.21 若├[X[YZ]]，則├[Y[XZ]]。

證明：

1 [X[YZ]] 前提

2 [[X[YZ]][[XY][XZ]]] Ax2

3 [[XY][XZ]] 1、2，MP

4 [[[XY][XZ]][Y[[XY][XZ]]]] Ax1

5 [Y[[XY][XZ]]] 3、4，MP

6 [[Y[[XY][XZ]]][[Y[XY]][Y[XZ]]]] Ax2

7 [[Y[XY]][Y[XZ]]] 5、6，MP

8 [Y[XY]] Ax1

9 [Y[XZ]] 7、8，MP

子程序1.11 若├X，則├((X))。

證明：

1 [[((X))(((X)))][[((X))((X))](X)]] Ax3

2 [[[((X))(((X)))][[((X))((X))](X)]]

[(((X)))[[((X))(((X)))][[((X))((X))](X)]]]] Ax1

3 [(((X)))[[((X))(((X)))][[((X))((X))](X)]]] 1、2，MP

4 [[(((X)))[[((X))(((X)))][[((X))((X))](X)]]]-

[[(((X)))[((X))(((X)))]][(((X)))[[((X))((X))](X)]]]] Ax2

5 [[(((X)))[((X))(((X)))]][(((X)))[[((X))((X))](X)]]] 3、4，MP

6 [(((X)))[((X))(((X)))]] Ax1

7 [(((X)))[[((X))((X))](X)]] 5、6，MP

8 [[(((X)))[[((X))((X))](X)]][[(((X)))[((X))((X))]][(((X)))(X)]]] Ax2

9 [[(((X)))[((X))((X))]][(((X)))(X)]] 7、8，MP

10 [(((X)))[((X))((X))]] 子程序4.12

11 [(((X)))(X)] 9、10，MP

12X前提

13 [X[(((X)))X]] Ax1

14 [(((X)))X] 12、13，MP

15 [[(((X)))(X)][[(((X)))X]((X))]] Ax3

16 [[(((X)))X]((X))] 11、15，MP

17 ((X)) 14、16，MP

通過這些子程序?qū)⑾鄳?yīng)主程序中的每一步都落實(shí)到具體的3條公理和推理規(guī)則MP上。

四、嵌入程序

如果輸入的目標(biāo)就是待證明定理即主程序的輸入，則直接使用子程序即可完成定理的化歸與證明；如果輸入的目標(biāo)不是待證明定理即不是主程序的輸入，而是其子公式，則需要借助嵌入程序完成將子程序楔入主程序的工作。

以主程序中的規(guī)則1.11為例，如果待證定理就是形如((X))的公式，則直接使用子程序1.11即可完成由((X))到X的化歸；如果輸入的目標(biāo)((X))僅僅是待證定理的子公式，則需要借助嵌入程序1.11完成將子程序1.11楔入主程序的工作。

如果((X))不是待證明定理即不是主程序的輸入，而僅僅是待證定理的子公式，則需要遞歸證明3種情況：(1)作為否定式的子公式，即主程序的輸入是(((X)))；(2)作為蘊(yùn)涵式前件的子公式，即主程序的輸入形如[((X))Y]；(3)作為蘊(yùn)涵式后件的子公式，即主程序的輸入形如[Y((X))]。因此，相應(yīng)地需要3個(gè)嵌入子程序。

嵌入程序1.11(1)若├(X)，則├(((X)))。

這是子程序1.11的一個(gè)特例，證明與其類似。

嵌入程序1.11(2)若├[XY]，則├[((X))Y]。

證明：

1 [[((X))[XY]][[((X))X][((X))Y]]] Ax2

2 [[[((X))[XY]][[((X))X][((X))Y]]][[XY][[((X))[XY]]

[[((X))X][((X))Y]]]]] Ax1

3 [[XY][[((X))[XY]][[((X))X][((X))Y]]]] 1、2，MP

4 [[XY][[((X))[XY]][[((X))X][((X))Y]]]]

[[[XY][((X))[XY]]][[XY][[((X))X][((X))Y]]]]] Ax2

5 [[[XY][((X))[XY]]][[XY][[((X))X][((X))Y]]]] 3、4，MP

6 [[XY][((X))[XY]]] Ax1

7 [[XY][[((X))X][((X))Y]]] 5、6，MP

8 [XY] 前提

9 [[((X))X][((X))Y]] 7、8，MP

10 [[(X)((X))][[(X)(X)]X]] Ax3

11 [[[(X)((X))][[(X)(X)]X]][((X))[[(X)((X))][[(X)(X)]X]]]] Ax1

12 [((X))[[(X)((X))][[(X)(X)]X]]] 10、11，MP

13 [[((X))[[(X)((X))][[(X)(X)]X]]][[((X))[(X)((X))]]

[((X))[[(X)(X)]X]]]] Ax2

14 [[((X))[(X)((X))]][((X))[[(X)(X)]X]]] 12、13，MP

15 [((X))[(X)((X))]] Ax1

16 [((X))[[(X)(X)]X]] 14、15，MP

17 [[((X))[[(X)(X)]X]][[((X))[(X)(X)]][((X))X]]] Ax2

18 [[((X))[(X)(X)]][((X))X]] 16、17，MP

19 [((X))[(X)(X)]] 子程序4.12

20 [((X))X] 18、19，MP

21 [((X))Y] 9、20，MP

嵌入程序1.11(3)若├[YX]，則├[Y((X))]。

類似嵌入程序1.11(2)可證。

嵌入程序1.11(1)～1.11(3)可統(tǒng)一表示為嵌入程序1.11。

嵌入程序1.11若├R{X}，則├R{((X))}。

類似地，對(duì)于其他主程序，除了子程序之外，也存在對(duì)應(yīng)的嵌入程序。例如，對(duì)于規(guī)則2.13，有相應(yīng)的子程序1.23和嵌入程序2.13。

子程序2.13若├[(X)Y]，則├[(Y)X]

嵌入程序2.13若├R{[(X)Y]}，則├R{[(Y)X]}。

對(duì)于嵌入程序2.13，同樣包括3個(gè)嵌入子程序：

嵌入程序2.13(1)若├([(X)Y])，則├([(Y)X])。

嵌入程序2.13(2)若├[[(X)Y]Z]，則├[[(Y)X]Z]。

嵌入程序2.13(3)若├[Z[(X)Y]]，則├[Z[(Y)X]]。

五、能行證明程序及其示例

基于前述化歸規(guī)則、子程序和嵌入程序可以給出從公理和MP規(guī)則出發(fā)的定理能行證明的基本程序：

(一)化歸

1．對(duì)于任意一個(gè)待證定理Th10，交替、反復(fù)使用雙否消去規(guī)則和否定內(nèi)移規(guī)則，將其化歸為一個(gè)基蘊(yùn)涵式Th11。

2．通過反復(fù)使用移動(dòng)、排序規(guī)則盡可能將Th11中有相同、相近字母的基式調(diào)整至前后相鄰的位置，得到Th12。

3．使用合并規(guī)則將公式Th12化簡(jiǎn)得到Th13。

4．反復(fù)使用上述1～3步驟進(jìn)行操作，直至得到可使用歸約規(guī)則Th14。

5．使用歸約規(guī)則將Th14化歸為形如[YY]的公式。

(二)證明

對(duì)于化歸進(jìn)行的每一步使用子程序和嵌入程序逆向完成證明。其主要步驟如下：

1．使用子程序5.01完成證明[YY]；

2．對(duì)于通過化歸而得到的Th14，則其必形如[X[Y[(Y)Z]]]或者[X[YY]]，可對(duì)其分別使用子程序4.11或者4.12完成由[YY]到[X[Y[(Y)Z]]]或者[X[YY]]的證明；

3．對(duì)于使用合并規(guī)則而得到的Th13，當(dāng)其輸入(輸出)的對(duì)象即為輸入(輸出)時(shí)，使用子程序完成由Th13到Th12的證明；當(dāng)其輸入(輸出)的對(duì)象為輸入(輸出)的子公式時(shí)，使用子程序和嵌入程序完成由Th13到Th12的證明。

4．對(duì)于使用移動(dòng)、排序規(guī)則而得到的Th12，當(dāng)其輸入(輸出)的對(duì)象即為輸入(輸出)時(shí)，使用子程序完成由Th12到Th11的證明；當(dāng)其輸入(輸出)的對(duì)象為輸入(輸出)的子公式時(shí)，使用子程序和嵌入程序完成由Th12到Th11的證明。

5．對(duì)于使用雙否消去規(guī)則和否定內(nèi)移規(guī)則而得到的Th11，當(dāng)其輸入(輸出)的對(duì)象即為輸入(輸出)時(shí)，使用子程序完成由Th11到Th10的證明；當(dāng)其輸入(輸出)的對(duì)象為輸入(輸出)的子公式時(shí)，使用子程序和嵌入程序完成由Th11到Th10的證明。

我們以一些定理的證明來作為示例。

定理5.11├[[(A)A]A][14]。

首先對(duì)其進(jìn)行化歸：

1 [[(A)A]A]輸入

2 [(A)([(A)A])] 1，規(guī)則2.14

3 [(A)(A)] 2，規(guī)則3.11

然后根據(jù)相應(yīng)的子程序或嵌入程序并逆向使用化歸程序完成證明，其基本步驟是：

1．使用子程序5.01證明[(A)(A)]；

2．使用子程序3.11證明[(A)([(A)A])]；

3．使用子程序2.14證明[[(A)A]A]。

為了簡(jiǎn)潔顯示證明程序，先證明兩個(gè)引理。在定理嚴(yán)格的公理證明之中，根據(jù)需要，這些證明只需適當(dāng)替換即可插入到完整的證明之中，從而還原為公理證明。

引理5.01若├Y，則├[XY]。

證明：

1Y前提

2 [Y[XY]] Ax1

3 [XY] 1、2，MP

引理5.02├[((X))X]。

證明：

1 [[(X)((X))][[(X)(X)]X]] Ax3

2 [[[(X)((X))][[(X)(X)]X]][((X))[[(X)((X))][[(X)(X)]X]]]] Ax1

3 [((X))[[(X)((X))][[(X)(X)]X]]] 1、2，MP

4 [[((X))[[(X)((X))][[(X)(X)]X]]][[((X))[(X)((X))]]

[((X))[[(X)(X)]X]]]] Ax2

5 [[((X))[(X)((X))]][((X))[[(X)(X)]X]]] 3、4，MP

6 [((X))[[(X)(X)]X]] Ax1

7 [((X))[[(X)(X)]X]] 5、6，MP

8 [[((X))[[(X)(X)]X]][((X))[(X)(X)]][((X))X]]] Ax2

9 [((X))[(X)(X)]][((X))X]] 7、8，MP

10 [(X)(X)] Ax1

11 [((X))[(X)(X)]] 10，引理5.01

12 [((X))X] 9、11，MP

引理5.03若├[X[YZ]]，則├[[XY][XZ]]。

至此，可以給出定理5.11的公理證明如下：

證明：

1 [(A)(A)] 子程序5.01

2 [(([(A)A]))[(A)(A)]] 1，引理5.01

3 [(A)[(([(A)A]))(A)]] 2，子程序2.21

4 [[(([(A)A]))(A)][[(([(A)A]))A]([(A)A])]] Ax3

5 [(A)[[(([(A)A]))(A)][[(([(A)A]))A]([(A)A])]]] 4，引理5.01

6 [[(A)[(([(A)A]))(A)]][(A)[[(([(A)A]))A]([(A)A])]]] 5，引理5.03

7 [(A)[[(([(A)A]))A]([(A)A])]] 3、6，MP

8 [[(A)[(([(A)A]))A]][(A)([(A)A])]] 7，MP

9 [(([(A)A]))[(A)A]] 引理5.02

10 [(A)[(([(A)A]))A]] 9，子程序2.21

11 [(A)([(A)A])] 8、10，MP

12 [[(A)([(A)A])][[(A)[(A)A]]A]] Ax3

13 [[(A)[(A)A]]A] 11、12，MP

14 [[(A)A][[(A)[(A)A]]A]] 13，引理5.01

15 [[[(A)A][(A)[(A)A]]][[(A)A]A]] 14，引理5.03

16 [[(A)A][(A)[(A)A]]] Ax1

17 [[(A)A]A] 15、16，MP(1)對(duì)于定理[[(A)A]A]，存在更簡(jiǎn)潔的基于公理和MP規(guī)則的證明：1 [[(A)[[B(A)](A)]][[(A)[B(A)]][(A)(A)]]] Ax22 [(A)[[B(A)](A)]] Ax13 [[(A)[B(A)]][(A)(A)]] 1、2，MP4 [(A)[B(A)]] Ax15 [(A)(A)] 3、4，M6 [[(A)(A)][[(A)A]A]] Ax37 [[(A)A]A] 5、6，M這說明能行證明方法提供了一個(gè)可操作的證明方法，但未必是最簡(jiǎn)單的證明方法。

在上述公理證明中，第1步是由子程序5.01完成的，第2至11步完成的實(shí)際上是子程序3.11的一個(gè)代入，第12至17步完成的是子程序2.14的一個(gè)代入。

六、余論

子程序、嵌入程序都是定理證明程序；而化歸主程序則和證明的方向相反，在完成化歸之后，再完善定理證明時(shí)需要沿著化歸程序逆向進(jìn)行。

本文給出的是定理自動(dòng)證明的程序大綱，后續(xù)還可進(jìn)行具體的程序設(shè)計(jì)，進(jìn)而完成基于本文思想的自動(dòng)定理證明器。

如果增加構(gòu)建一個(gè)輔助程序，在待證定理的證明中對(duì)已經(jīng)證明的定理可以直接調(diào)用，這樣可以大大簡(jiǎn)化定理的自動(dòng)證明。

關(guān)于程序規(guī)則的合理性說明：對(duì)于任一給定待證的定理，通過使用雙否消去規(guī)則、否定內(nèi)移規(guī)則、移動(dòng)排序規(guī)則、合并規(guī)則之后，必定可以等值地化歸為一個(gè)形如[X[Y[(Y)Z]]]或者[X[YY]]的公式。因?yàn)槿羝洳蝗?，則在其等值化歸為形如[X1[X2…[XnY]…]]的公式中，Xn不同于Y并且在X1、X2、…、Xn中不存在相互否定的公式，因此必定可以構(gòu)造一個(gè)賦值v，使得(X1)v=(X2)v=…=(Xn)v=1，而(Y)v=0，因而[X1[X2…[XnY]…]]v=0，這與原公式是待證定理矛盾。因此，待證定理必定可以化歸為一個(gè)形如[X[Y[(Y)Z]]]或者[X[YY]]的公式，進(jìn)而可以進(jìn)一步利用歸約規(guī)則將其化歸為形如[YY]的公式，并進(jìn)而得到證明。

使用劃歸方法對(duì)系統(tǒng)的內(nèi)定理進(jìn)行能行證明，這與通常訴諸公理及變形規(guī)則之特征的能行證明方法不同，因?yàn)樵摲椒ǖ幕舅枷氩皇芟到y(tǒng)內(nèi)具體公理和規(guī)則的限制(盡管文中為了說明方便，使用了一個(gè)具體的公理系統(tǒng))(2)當(dāng)然，對(duì)于不同于文中的公理系統(tǒng)，本文給出的證明程序需要適當(dāng)調(diào)整，即只需對(duì)其中的雙否消去規(guī)則、否定內(nèi)移規(guī)則、移動(dòng)排序規(guī)則、合并規(guī)則和歸約規(guī)則給出系統(tǒng)內(nèi)的證明子程序。而整個(gè)能行證明的主體框架和化歸的基本思想是沒有改變的。。所以，該方法比較而言，更具一般性，因而也更加容易推廣到其他公理系統(tǒng)之中。