通過證明系統進行證明的方法大致可分為基於公理系統和基於規則系統兩種基本子類。這兩種系統都有專門的名稱，嚴格地說，基於公理進行推理推演、並具有句法要求的證明系統是形式公理系統，簡稱形式系統，大致上稱之為“希爾伯特風格的證明”系統；而僅僅基於句法規則進行轉換的證明系統即自然演繹系統，大致上稱之為“根岑風格的證明”系統(“希爾伯特風格”和“根岑風格”還有其他區別，但核心的區別在於此)。質言之，形式系統以公理作為前提來證明命題；自然演繹系統以規則通過語法形式轉換來證明命題——可以沒有公理，只有規則。
基本介紹
- 中文名：方法系統化證明
- 外文名：Method systematic proof
- 所屬領域：數學
- 分類：基於公理系統和基於規則系統
- 起源：古希臘數學
- 最初使用者：泰勒斯
發展沿革,原理,
發展沿革
最早提出數學證明概念的人可能是畢達哥拉斯。他提出數學命題應該給予嚴格的證明。按照當時的數學證明方法，應指公理化證明。
亞里士多德的三段論證明系統是最早的自然演繹系統和形式系統——他不只提出了三段論推理形式，還給出了用規則推導出有效三段論的方法，這屬於自然演繹系統的證明方法；同時，基於三段論的第一格第一式(Babara)推導其他格式的三段論方法相當於把第一格第一式作為形式系統進行證明。
歐幾里德的公理系統較早並比較完善地創造了公理化數學證明的範例。這一影響是巨大的。後來的許多幾何學如希爾伯特幾何學、羅巴切夫斯基幾何學、黎曼幾何學都構建了公理系統。不僅在數學領域，對於科學而言，歐幾里德展示了科學作為陳述體系的邏輯圖景。例如，在物理學領域，牛頓的《自然哲學的數學原理》也是借鑑歐幾里德的公理系統的結構和方法寫成的，即命題是逐次、累積證明的。
在現代，在弗雷格和羅素已經建立了形式化的邏輯演算體系背景下，由於希爾伯特提出了數學公理化的倡議，使得公理化成為數學的一個重要目標，公理化方法由此也應該成為數學的一個基本方法。
希爾伯特的公理化思想主要地陳述於他的《數學問題——在1900年在巴黎國際數學家代表大會上的講演》，以及1922年他在德國的一次數學會議上就這些問題提出的研究大綱。在前一篇文章中，希爾伯特提出了23個待解的數學問題，其中第2個問題是“算術公理的相容性”。他說：“在研究一門科學的基礎時，我們必須建立一套公理系統，它包含著對這門科學基本概念之間所存在關係的確切而完備的描述。如此建立起來的公理同時也是這些基本概念的定義；並且，我們正在檢驗其基礎的科學領域裡的任何一個命題，除非它能夠從這些公理的有限步邏輯推理而得到，否則就不能認為是正確的。”第6個問題是“物理公理的數學處理”。在對這個問題的陳述中，他認為存在這樣一個問題，即如何“用同樣的方法藉助公理來研究那些數學在其中起重要作用的物理科學，首先是機率論和力學”。可以看出，希爾伯特認為存在一種可能，至少在數學物理科學中建立公理系統證明數學或物理科學(數學在其中起重要作用)命題。這實際上是一種將科學公理化的傾向。
隨著系統化證明方法的發展，產生了針對專門化的數學知識領域的形式系統。它是系統化證明方法的實例。例如，皮亞諾算術系統(PA)、希爾伯特的幾何證明系統，等等，這些證明系統的證明方法首先屬於系統化證明方法，還有針對特定領域的方法和關於特定領域的理論。同時，也建立了多個通用的自然演繹系統，如根岑的自然演繹系統。
原理
為推演出或者判定命題，可以通過給定的公理進行推演，也可以僅僅通過一些表述定理的語言的轉換規則對給定命題進行轉換，直至轉換為預期的結果。由此可以將證明系統劃分為兩個類別：基於公理的證明系統和基於轉換規則(簡稱為規則)的證明系統。它們具有相同的特點，都是依據一個符號集合實現證明，從而使證明成為一個基於原初系統(這個符號集合)的生成過程。換言之，這種證明是構造性的，它是由一個(有限符號的原初)系統構造的。
同時，這兩種系統也有區別，這種區別首先在於(原初的符號)系統的構成不同：一種必須包含公理集合，而另一種必須包含規則集合，並且在嚴格意義下基於規則的系統不要求系統必須預先有公理(但是不排除證明前或證明中加入公理)。當然，在很多情況下，一個證明系統可以將二者都包括在內。具體而言，用於推演的公理和用於轉換的規則之間的區別，以及由此導致的兩個系統的區別在於：
(1)一個具體的公理一般表示為命題常元(針對特定領域的特殊公理)：而規則一般將命題表示變元。因此，基於公理集合的證明系統允許包含具體命題(公理常元)——儘管並非所有的公理系統都包含命題常元：而基於規則證明系統一般不給出命題常元(除非針對某一專門命題制定規則，這意義就不大了)，基本上只給出命題變元。
(2)公理是永真的；規則允許不是永真的(進行某種轉換是否是永真轉換，則需要依據操作目的而定。雖然在很多情況下，規則是等值轉換，使得被轉換的原有的或真或假的邏輯值被保留，但是在很多情況下，規則是語法化的，無所謂真假轉換)。
(3)規則是語法化的，它是符號生成轉換規則；公理的推導允許是非語法化的，即它的轉換不必遵循語法規則，只是基於內容的轉換一一如歐幾里德公理系統中的公理，它們是與語法形式無關的，因此它們是內容化的。
(4)公理是對象語言表述的：規則是衍語言表述的。例如，數學公理的陳述對象是數學世界的概念，關於“數”“空間”“+”“<”，等等。因此，在基於公理集合的證明系統中，一般包含有非邏輯符號(數學專用符號)。而規則陳述關於對象，其本身所使用的語言不是對象語言，而是衍語言，諸如“函詞”“命題”“參數”“蘊涵”“合取”之類。
