基本介紹
歐幾里德公理系統不是形式公理系統，即在歐幾里德公理系統中，一個公理或命題均以自然語言表述，這個公理或命題變換表述方式(形式有無變化)不影響系統證明的步驟和功能。它只是以其表述的內容由人來理解和運用(而後來的計算機需要形式化語言)，因此，命題在形式上與證明無關。
歐幾里德公理系統第一次將數學證明構造成這樣一個系統的功能，這個系統由以下幾個部分構成：
(1) 公設，它們是不證自明的、最一般化的幾何命題，它像“母命題”一樣生成(蘊涵)其他定理或命題。
(2) 公理，它們是不證自明的、最一般化的代數、數論的命題，也具有“母命題”一樣的功能。
(3) 命題，指由公設和公理證明的命題。
(4) 定義，定義也是一種命題，是系統給出的對於某一特徵的一種命名。
證明的系統是一個開放的累積系統：系統將公設和公理作為初始的知識庫，每證明一個命題就將其增加到這個知識庫，使得知識庫逐步擴大，作為證明其他命題的證明系統。
歐幾里德公理系統的10個公設和公理如下：
公設1：兩點可以決定一條直線。
公設2：直線可以沿其正反兩個方向無限延長。
公設3：在平面內，所有與某一定點的距離相等的點可構成一個圓。
公設4：凡直角都相等。
公設5：同一平面內一條直線和另外兩條直線相交，若在這條直線同側的兩個內角之和小於180°，則另外兩條直線一定相交。
公理1：等於同量的量彼此相等。
公理2：相等的量加某一量，其和仍相等。
公理3：相等的量減某一量，其差仍相等。
公理4：彼此能夠重合的幾何圖形是全等的。
公理5：整體大於部分。
由上述的10個公理和公設以及命題和定義構成的證明系統稱為 歐幾里德公理系統E 。
相關介紹
歐幾里德幾何公理系統是早期數學中最有影響的公理系統，大約提出於公元前3世紀。
近代的幾何公理系統力圖對歐幾里德幾何公理系統進行改進，其中最重要的一個方面是對幾何要素及其相關公理進行分類。這些工作首先由帕施(M.Pasch)的射影集合公理系統在1882年開始。此後，皮亞諾的幾何公理系統創立於1889年和1894年，在他的幾何公理系統中，分別建立了點、線、面、體的各種公理。此後不久，希爾伯特幾何公理系統受到皮亞諾公理系統和帕施的影響，於1898-1902年構造了新的幾何公理系統，集中體現在1899年出版的《幾何基礎》一書。
歐幾里德的公理系統E的結構是形式公理系統的前身，可以看出，對這一結構進行形式化的改進將構成形式公理系統，簡稱形式系統。這種形式化的改進包括：
(1)對表示被證命題的語言的符號進行明確規定，即增加初始符號部分，對表示所有被證命題的語言所使用的符號進行明確或進一步的說明。
(2)對表示被證命題的語言的語法進行明確規定，即增加公式的形成規則和變形規則兩個部分，前一個規則對表示所有被證命題的語言如何形成一個合式公式進行規定，後一個規則對表示所有被證命題的語言的形成的公式如何轉換進行規定，使得證明的過程是一個合式公式依照這一轉換規定進行轉換的過程。
歐幾里德的公理系統E展示了數學知識之間的邏輯關係(作為邏輯運算的原子命題之間構成的關係，特別是蘊涵關係、命題之間的傳遞關係等)，它同時展示了數學證明可由少部分初始命題證明多個命題，這部分初始命題構成一個系統，並具有確定的結構(如上所述，包括公設、公理、定義，對於歐幾里德之後的系統，還可能加入斷言或命題作為公理的補充部分)和功能(持續不斷地證明命題使之加入己證明的知識庫，作為證明知識庫之外其他命題的知識基礎)。而證明的過程是這個系統的運行過程。
歐幾里德公理系統E證明了當時幾乎所有純數學命題(465個命題，包括幾何、代數和數論的定理)，但是E的完全性沒有被證明，即哪些數學命題(準確地說是符合哪些特徵的數學命題)是它能證明的，這個證明的範圍沒有得到描述和證明。
關於它的一致性討論較多。特別是對於第5公設是否成立促進了非歐幾何的誕生。但是在邏輯體系內，歐幾里德的公理系統E並未被證明是不一致的；換言之，非歐幾何的定理不能在邏輯上否定第5公設 。
套用舉例
例1《幾何原本》中的一個幾何命題的證明。命題1.29(《幾何原本》中的編號)：一條直線與兩條平行線相交，所形成的內錯角相等，同位角相等，同旁內角互補。
圖1已知：直線AB//直線CD，直線EF與AB和CD相交於GH，如圖1所示。
求證：
歐幾里德公理系統①：
歐幾里德公理系統②；
歐幾里德公理系統③。
證明：
因為平面內一直線與另兩條直線相交，如果第一個直線某一側的兩個內角之和小於180°，則這兩條直線經過無限延長後必在這一側相交(根據公設5)，而已經假設二直線平行，所以
歐幾里德公理系統(根據公設5，結論③)
因為
歐幾里德公理系統(根據下文命題2)
所以
歐幾里德公理系統(根據公理1，結論①)
因為
歐幾里德公理系統(根據下文命題3)
所以
歐幾里德公理系統(根據公理1，結論②)
命題1 過直線上的一個點可做該直線的垂線 。
命題2兩直線相交鄰角等於180 。
註：套用了公理1、公理2和命題1(“過直線上的一個點可做該直線的垂線”)。
命題3兩直線相交對等角相等。
註：套用了命題2、公理1、公理3和公設4 。
