1、關于形式化的討論第2、3章證明了每命題形式都可以通過等值變換成各種范式用真值表方法和范式，回答了命題邏輯中很多有重要意義的問題，如：判定任一給定的命題形式是不是重言式(常真的)、矛盾式(常假的)；一命題形式是不是另一些命題形式的邏輯后承；兩個任給的命題形式是否等值以及如何判定一個推理形式是否正確，等等。但是，真值表方法有它的局限性，它沒有把所有的重言式作為一個整體來研究，而邏輯中其它更復雜的部分也不能用真值表方法來處理。公理方法是研究命題邏輯的另外一種方法，通公理方法建立命題邏輯的形式系統命題演算。公理系統 從一些公理出發，應用邏輯規則，推導一系列定理，這樣形成的演繹體系稱為公理系統。歐氏幾何

2、就是一個著名的古典公理系統。 公理系統首先包括一組特別挑選出來的命題稱為公理，也叫作初始命題。公理是不加證明而接受作為系統的出發點的。系統中其余的命題都從公理出發經證明推導出來，稱為定理。公理的選擇必須滿足某些一般的條件，如公理必須明確地規定所包含的概念的意義，并且容易理解；一組公理要能充分地刻劃所研究對象的恃征；是協調的(不會導致矛盾的)，等等。在現代公理系統中，選作公理的命題其真實性不一定是最明顯的。 公理系統包括一組不加定義的概念，稱為基本概念或初始概念。其余的概念由基本概念定義，稱為派生概念。基本概念的意義由公理明確地陳述和規定。 現代公理系統和古典公理系統的一個重大差別是，對于現代公

3、理系統，可以有多種不同的概念都使得公理為真，或者說可以對系統作不同的解釋。例如，等價關系理論就是現代公理系統的一個例子。 例 等價關系理論建立在下面三個公理的基礎上（xRy讀作“x等價于y”或“x與y等價”）。 (E1)對所有x，xRx； (E2)對所有x和y，如果xRy，則yRx； (E3)對所有x，y和z，如果xRy并且yRz，則xRz。 令A是一非空集合，R是A中的一個二元關系。二元組A，R稱為一個結構。我們稱R是A中的一個等價關系，A，R是一個等價結構如果公理(E1)-(E3)被滿足的話。(E1)-(E3)不是關于某一個特定的等價結構的公理，其中的R可以作不同的解釋。例如，以S表示命題

4、形式的集合，把R解釋為命題形式之間的等值關系“=”；以自然數集合N為論域，把R解釋為自然數的相等關系“=”；以整數集合Z為論域，把aRb解釋為a-b能被5整除(記為“R5”)，那么S，=，N，Z，R5都是等價結構。形式系統形式系統是完全形式化的公理系統。對公理系統的研究，可以采取兩種不同的觀點：一種是把公理、定理等等看作是語句，另種足把公理理解為由語句所表達的意義。前者是對公理系統的語法研究；后者是對公理系統的語義研究。形式系統是公理系統的語法部分，使用人工語言，用專門的符號表示概念，把公理和定理都變換成一些符號公式，對這些具體對象進行研究。形式系統和通常的公理系統的另一個不同之點是，普通公理

5、系統不把從公理推導定理(證明定理)所用的邏輯規律(推理規則)包括系統在本身之中，對于哪些證明方法是可以使用的沒有明確的規定。而在形式系統中對此有明確的規定。一個形式系統包括三個組成部分。第一部分是語言（形式語言），通常是一種人工語言。語言的選擇應當盡可能使得語句的結構能反映它們的意義。建立一個語言首先是確定它的符號（初始符號）。初始符號相當于普通拼音文字中的字母，也稱為字母表。當對符號加以解釋時，其中某些符號就是公理系統的初始概念。符號的數目一般是無窮的，可以由有窮個初始符號進行構造。符號的有窮序列(有窮長的符號串)稱為表達式。某一表達式中符號的數目（包括重復數）稱為該表達式的長度。一個表達式

6、(不算單個符號自身)也可能在另一表達式中出現。例如，“好讀書”和“好讀書不好讀書”是漢語中的兩個表達式，前一表達式在后一表達式中出現兩次。表達式中有一部分被專門區別開來。在有的形式語言中，這樣被區分開來的表達式包括兩類，一類稱為項，一類稱為合式公式。一個語言的符號和公式確定時，語言得到確定。建立一個語言就是確定它的符號和形成規則。語言是純語法的對象。形式系統的第二個組成部分是它的公理。公理是從系統公式中挑選出來作為推導系統中其余定理的出發點的部分公式。形式系統的第三個組成部分是推理規則，也稱變形規則。推理規則用于從公理得出定理。每一條推理規則都規定：在一定條件下，從若干稱為前提的公式能推出一個

7、稱為結論的公式。當一個推理的前提是公理或者是已經應用推理規則從公理得出的結論，那么應用一個推理規則得出的結論稱為定理。一個形式系統的定理可以定義為：(1)一個形式系統的公理是它的定理；(2)如果所有的前提都是定理，那么應用它的一個推理規則得出的結論是它的定理。并且只有根據(1)和(2)這兩條能確定它是定理的公式才是系統的定理。對于一個形式系統的定理可以更清晰地描述如下：設S0是系統的公理的集合，根據(1) S0是能夠確定為定理的公式集合。設S1是只以S0中的公式作前提應用推理規則得出的結論集合，根據(2)S1是能夠確定為定理的公式集合。設S2是只以S1中的公式作前提應用推理規則得出的結論集合，

8、根據(2)S2是能夠確定為定理的公式集合。 用同樣的方法構造集合S3，S4，.令S¥是以S0，S1，S2.中的公式作前提應用推理規則得出的結論集合，根據(2)S¥ 是定理集合。用同樣的方法繼續構造下去，直到根據(2)再也不能得到新的定理為止。這樣得到了一個形式系統的全部定理上述方式的定義稱為廣義歸納定義。一個歸納定義通過給出一組規則(法則)，由這些規則確定某一類對象組成的一個集合。這些規則中的第一條規定某些對象屬于該集合，其余各條都規定如果某些對象屬于該集合，那么另外的一個怎樣的對象屬于該集合。形式語言的(合式)公式的形成規則是一個關于合式公式的歸納定義。歸納定義具有這樣的

9、特點：要證明歸納定義所確定的某一類對象中的每一個都有某個性質，只需證明滿足定義中陳述的規則的對象都有該性質。例如，要證明一個形式系統的每一定理都有性質P，只需要證明滿足對定理的定義規則的公式都有性質P。即只需要證明：(1')形式系統的每一公理都有性質P；(2')如果一個推理規則的所有前提都有性質P，結論也有性質P(推理規則保持性質P)。用這個方法所作的證明稱為對于定理的歸納證明。(1')稱為基始，(2')稱為歸納步驟。(2')中的假設：推理規則的所有前提都有性質P，稱為歸納假設。類似地，要證明每一個合式公式都有某個性質，只需對合式公式作歸納證明。歸納證明

10、是一個很重要應用很廣的證明方法。一個形式系統由語言(包括初始符號和形成規則)、公理和推理規則這樣三部分組成。系統中的其它對象：合式公式(或者還有項)和定理都是在系統內逐步生成的。公式由符號和形成規則生成，定理由公理和推理規則生成。每一公式和定理都有一個生成序列，一個公式的生成序列是由有窮個公式組成的，其中每一個或者是由公式形成規則直接確定為公式的，或者從前面的公式根據形成規則形成的，最后一個是由這序列生成的公式。公式是有窮長的符號序列，所以總能在有窮步內生成，生成序列的長度是有窮的。定理是由公理和推理規則生成，每一推理規則的前提的數目是有窮的。定理的生成序列稱為證明，其長度也是有窮的。一個證明

11、是一有窮長的公式序列，其中每一個公式或者是一個公理，或者是以序列中在前的公式作前提的一個推理規則的結論。如果一個公式A是一個證明P的最后的公式，就說P是A的一個證明，并說A是一個定理。一形式系統的一個公式是系統中的定理當且僅當存在它的一個證明。每一定理都有一個證明：對定理作歸納證明，一個公理自身是它的一個證明，所以每一公理是有證明的。如果一個定理是以某些定理作前提的推理規則的結論，根據歸納假設，這些作前提的定理都是有證明的。這樣把這些證明放在一起構成一個公式序列，把那個公式(定理)放在這序列的最后，就得到這個公式(定理)的一個證明。反過來，如果一個公式是有證明的，它是一個證明的最后的公式，根據

12、定理和證明的定義，它就是個定理。在一個形式系統中，對于下列各點：(1)任一符號是不是一初始符號；(2)任一有窮長的符號序列是不是合式的；(3)任一公式是不是一個公理；(4)任一公式是不是以給定的公式作前提的某個推理規則的結論；(5)任一有窮長的公式序列是不是一個證明，也就是說，序列中的每一公式是不是一個公理，或者是不是以序列中在前的公式作前提的推理規則的一個結論。都要求有一個機械的方法，能在有窮步內進行判定。在形式系統中，上述各點都是能夠判定的。一般不能機械地判定任一公式是不是一個定理。要求判定一個公式是不是定理，需要給出它的一個證明，確定它是定理，或者證明它不是定理即它是沒有證明的，所有的證

13、明都不是它的證明。存在機械的方法判定一個公式是不是定理的系統(理論)，稱為是可判定的。內容豐富的系統一般是不可判定的。語法和語義形式系統是把普通公理系統形式化的結果。普通的公理系統都是有解釋的理論，其中的公理、定理等等都是有意義的。一個形式系統是一個公理系統的語法部分。在把一個公理系統形式化時，用特定的符號表示公理系統中的概念，用符號公式表示公理系統中的命題，而把公理系統的內容抽象。在形式系統中，處理的只是符號、公式、公式的符號組合的變換等等，完全不涉及內容和意義。推理實際上就是對公式(符號組合)所作的變形或符號變換。從給定的前提能不能得出某個結論，實際上就是根據變形(推理)規則，從給定的公式

14、經過符號變換能不能得出(變成)某個公式。這種語法研究的優點是，符號、公式等等都是具體的對象，是完全確定的，不會引起不同理解，不會造成歧義并且容易掌握，能更精確地處理。而意義是抽象的，往往比較難于理解和掌握，不同的人在理解上很容易不一致。語法研究包括可證明性、協調性等重要概念和問題。在把一個有內容的理論形式化，建立一個形式系統時，在選擇形式系統的語言時，應盡可能使得系統的語句(公式)的結構能反映它們的意義。經解釋后某些符號就成為概念，公式成為有意義的句子。對形式系統的解釋，關于表達式的意義、表達式與它們所反映的對象之間的關系的研究，屬于語義的研究。語義研究包括真假、可滿足性、意義等等概念和問題。

15、由語義研究建立的理論成為語義理論或者語義學關于公理系統P 合式公式的定義是一個歸納定義。因此，要證明所有的公式都有某個性質，可以對公式作歸納證明。這個證明方法稱為施歸納于公式的結構，具體地說，要證明所有公式有某個性質，只要證明以下三點：(1) 所有原子公式都有這個性質；(2) 對任何A，如果A有這個性質，則 ØA有這個性質；(3) 對任何A和B，如果A和B有這個性質，則(A®B)有這性質。P的公理和推理規則P的公理 凡是有下列形式的P的公式都是P的公理：(A1) A®(B®A)(A2)(A®(B®C)®(A®B)&

16、#174;(A®C)(A3) (ØA®ØB)®(ØA®B)®A)(A2)稱為蘊涵詞分配律，即蘊涵詞對蘊涵詞自身是可分配的(A3)稱為反證律，它反映通常的反證法，相當于：假設A是假的(即假設ØA)，就引出一個矛盾，即得出B并且非B(ØA蘊涵B，ØA蘊涵ØB)，那么就可以肯定A。P的定理我們也可以用另一種方式，即用歸納定義來定義P的定理：(1) P的每一公理是P的定理；(2) 如果分離規則的前提A1，A2是定理，B是應用分離規則從A1和A2得出的結論，則B是定理。要證明P的所有定

17、理有性質P，需要證明：(1) 每一公理有性質P；(2) 如果A1，A2有性質P，B是應用分離規則從A1，A2得出的結論，則B有性質P定理 P中有1A®A (同一律)2(B®C)®(A®B)®(A®C)3(A®B)®(B®C)®(A®C) (蘊涵詞傳遞律)4(A®(B®C)®(B®(A®C)證明導出規則下面引進若干規則，稱為導出的推理規則，簡稱導出規則。這些規則從P中的公理、定理和分離規則導出。導出規則具有與分離規則同樣的性質：如果一個規

18、則的前提是定理，那么應用規則得出的結論也是定理。應用導出規則可以簡化證明。導出規則1 從A，可推出B®A導出規則2 從A®(B®C)，可推出(A®B)®(A®C)導出規則3 從ØA®ØB和ØA®B，可推出A導出規則4 從A®B和B®C可推出A®C導出規則5 從A®(B®C)，可推出B®(A®C)定理 P中有5A®(A®B)®B)6ØØA®A (雙重否定律)7

19、A®ØØA8(ØA®ØB)®(B®A)9(ØA®B)®(ØB®A)10(A®B)®(ØB®ØA)11(A®ØB)®(B®ØA)12(A®ØB)®(A®B)® ØA) (歸謬律)證明演繹定理我們將證明一個重要的語法定理演繹定理。應用演繹定理可以大大簡化一個定理的建立過程。有前提的推演在有前提的推演中，除了公理以外，還以其它的公式作為前提。定義 給定一組公式 G=A1，A2， An，一個有窮長的公式序列B1,B2,Bm 稱為是(P中的)從前提(假設) A1，A2， An 的一個推演，如果每一個Bi(1£i£m)都滿足以下條件之一：(1) BiÎG；(2) Bi是P的一個公理(A1-A3之一)；(3) Bi是由Bj和Bk(1£j<k<i)應用分離規則得到的。此時稱推演為關于公式Bm的推演，公式Bm稱為“G可推演”的，記 GBm，并稱Bm是該推演的結論。從定義可