杜國平

(1.中國社會科學院大學 哲學院， 北京 102488； 2.中國社會科學院 哲學研究所， 北京 100732)

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

一、基元、基式

本文以如下公理系統(tǒng)L但不限于這一系統(tǒng)作為討論的標的之一。該系統(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]。

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

(A) =def〈AA〉

[AB] =def〈A〈BB〉〉

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

Ax1 [B[CB]]

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

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

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

如上所示，本文之所以使用括號表示法，一方面使用括號表示法可以精簡公式，另一方面通過定義引入其他括號，既實現(xiàn)了對不同聯(lián)接詞靈活的表達，同時也不影響直觀閱讀[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對于形如[X1[X2…[XnY]…]]的公式，稱X1、X2、…、Xn為其若干前件，稱Y為其后件。

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

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

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

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

RX RY 規(guī)則0.01

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

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

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

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

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

2.否定內移規(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])中的否定內移問題。但是因為：(1)單獨的公式([X[YZ]])以及([([XY])Z])均不是有效式(因為如果([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])沒有比其更簡單的單一公式形式。因此，對于形如([X[YZ]])以及([([XY])Z])的公式，其中的否定內移比較復雜。需要考慮其分別作為一個蘊涵式的前、后件的情況。

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

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

(二)移動、排序規(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

通過對反復使用雙否消去規(guī)則、否定內移規(guī)則得到的公式再反復使用移動、排序規(guī)則可實現(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

通過對反復使用雙否消去規(guī)則、否定內移規(guī)則、移動、排序規(guī)則得到的公式再反復使用合并規(guī)則可實現(xiàn)將其化歸為若干個經過簡化的基式或者若干個其若干前件和后件均為基式的蘊涵式。

(四)歸約規(guī)則

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

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

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

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

三、子程序

上述主程序給出了將任一公式化歸為形如[YY]公式的綱要，對于其中每一個規(guī)則給出的每一步程序的具體實現(xiàn)還需要更加精細的子程序以實現(xiàn)其由公理和推理規(guī)則證明定理的具體步驟。下面不一一給出細節(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

通過這些子程序將相應主程序中的每一步都落實到具體的3條公理和推理規(guī)則MP上。

四、嵌入程序

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

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

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

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

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

嵌入程序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))}。

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

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

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

對于嵌入程序2.13，同樣包括3個嵌入子程序：

嵌入程序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．對于任意一個待證定理Th10，交替、反復使用雙否消去規(guī)則和否定內移規(guī)則，將其化歸為一個基蘊涵式Th11。

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

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

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

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

(二)證明

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

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

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

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

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

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

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

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

首先對其進行化歸：

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

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

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

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

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

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

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

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

引理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)對于定理[[(A)A]A]，存在更簡潔的基于公理和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這說明能行證明方法提供了一個可操作的證明方法，但未必是最簡單的證明方法。

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

六、余論

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

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

如果增加構建一個輔助程序，在待證定理的證明中對已經證明的定理可以直接調用，這樣可以大大簡化定理的自動證明。

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

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