伯矩鬲

[拼音]：gonglihua he xingshihua

[英文]：axiomatization and formalization

研究演繹科學理論和構造演繹系統的兩種方法。它們被廣泛應用於現代邏輯和數學研究中。

公理化

把一個科學理論公理化，就是用公理方法研究它，建立一個公理系統。每一科學理論都是由一系列的概念和命題組成的體系，公理化的實現就是：

（1）從它的諸多概念中挑選出一組初始概念，即不加定義的概念，該理論中的其餘概念，都由初始概念通過定義引入，即都用初始概念定義，稱為匯出概念；

（2）從它的一系列命題中挑選出一組公理，即不加證明的命題，而其餘的命題，都應用邏輯規則從公理推演出來，稱為定理。應用邏輯規則從公理推演定理的過程稱為一個證明，每一定理都是經由證明而予以肯定的。由初始概念、匯出概念、公理以及定理構成的演繹體系，稱為公理系統。其中，初始概念和公理是公理系統的出發點。

公理方法經歷了從古代的實質公理學到現代的形式公理學的發展過程。

公理系統相應地區分為古典公理系統、現代公理系統或稱形式公理系統。最有代表性的古典公理系統是古希臘數學家歐幾里得在《幾何原本》一書中建立的。第一個現代公理系統是D.希爾伯特於1899年提出的。他在《幾何基礎》一書中，不僅建立了歐幾里得幾何的形式公理系統，而且也解決了公理方法的一些邏輯理論問題。

古典公理系統的物件域即公理系統所研究的物件，是先於公理而給定的，概念是物件的反映，公理則反映對這些物件的認識，表達這類物件的重要性質和關係。古典公理系統的初始概念和公理都有直觀的具體內容，而系統的公理和定理是關於這物件域的真命題。從認識的發展來看，現代形式公理系統雖然一般也是從某種直觀理論得到的，並且通常有預先想到的解釋。但是，系統自身並不給初始概念予直觀的具體內容，它們的意義完全由公理規定，對初始概念和公理可以給予不同的解釋，可以刻劃多個不同的物件域，即有多個不同的物件域都可以使得一個公理系統的公理和定理為真，它們在不同的解釋下成為不同物件域的真命題。

公理系統要滿足某些一般要求，包括系統的一致性、完全性和範疇性，以及公理的獨立性。其中一致性是最重要的，其他幾個性質則不是每個公理系統都能滿足的，或可以不必一定要求的。

形式化

公理系統的進一步形式化不僅可以有不同的解釋，而且需要應用專門設計的人工符號語言，使一個理論更為精確化和嚴格化，也就是運用人工的表意符號語言陳述所要形式化的理論。這種人工語言稱為形式語言。把一個理論形式化就是把理論中的概念轉換為形式語言中的符號，命題轉換為符號公式，定理的推演轉換成符號公式的變形，並把一個證明轉換成符號公式的有窮序列。形式語言的符號和它們所表示的概念之間的對應是確定的，符號公式的結構反映它們的意見。把一個理論形式化後，就可以暫時完全撇開原來理論中的概念、命題的意義，而只從語言符號、公式結構（符號組合的形狀）方面研究。意義是抽象的，往往不容易精確理解和掌握。而符號和公式是有窮的具體的物件，能夠對其作更精確、更嚴格的研究，從而通過對具體物件的研究把握抽象的東西。

形式系統

把一個理論形式化的結果是建立形式系統。形式系統是形式化了的公理系統，它包括以下 3個部分：

（1）形式語言。規定一個形式語言，首先要列出各種初始符號，它們是形式語言的字母，其中一部分是初始概念，包括邏輯概念；然後再列出一組形成規則，形成規則規定怎樣由初始符號組合起來的符號序列是系統中的合式公式，只有合式公式才是有意義的命題，而不合式的符號序列則是無意義的。

（2）形式系統的公理。公理是挑選出來作為出發點的一組合式公式，它們經解釋後可以是真的命題。

（3）一組變形規則，也稱為推導規則。變形規則規定怎樣從一個或幾個合式公式經過符號變換而推匯出另一合式公式。形式系統的證明是合式公式的有窮序列，其中每一公式或是一公理，或者是從在前的公式根據變形規則推匯出來的。一個證明也稱作它的最後一個公式的證明，一個合式公式也是系統中的定理，當且僅當存在它的一個證明。

嚴格的形式化和形式系統的概念，與精確的機械的程式概念和能行可判定概念分不開。所謂機械的程式，每一步都是由事先給定的規則明確規定了的，規則規定了第一步如何作，在完成某一步之後下一步如何作，並且在有窮步後能夠結束。所謂能行可判定，是指對一類問題有一機械的程式，對任給該類中的問題，能在有窮步內確定它是否有某個性質，或者任給一物件能在有窮步確定它是否屬於該類。

對於形式系統的一個最重要的要求，就是有機械的程式並可能行地判定：

（1）任給一符號是不是系統中的初始符號；

（2）任給一符號的有窮序列是不是系統中的合式公式；

（3）任給一合式公式是不是公理；

（4）任給一合式公式是不是從給定的合式公式根據變形規則得到的；

（5）任給一合式公式的有窮序列是不是一個證明。根據這些要求，雖然一般地說，在形式系統中給定一公式時，並沒有一個機械程式找出它的證明，但只要任給一有窮的公式序列，就能機械地判明它是否確實是本系統中的一個正確的證明。這樣就可以對於一個形式化的公理系統的許多邏輯性質進行科學的研究。

明確的形式化和形式系統的概念是希爾伯特在20世紀20年代初提出的。形式化的明確提出和形式系統的建立，在公理學發展史上有著十分重大的意義。它標誌著以形式系統為研究物件的元邏輯或元數學的誕生，對現代邏輯科學的發展起了重大的作用。