邏輯演算

這類推理的正確性僅依賴於它們的形式,而與內容無關,例如三段論法。在這裏，概念、推理等被分解為最基本的元素，推理過程被表示為由開始公式出發根據某些具體規則而做的形式變形。

邏輯演算的思想，也就是數理邏輯最初的思想，首先由 G.W.萊布尼茨明確提出，又經 G.布爾、（F.L.）G.弗雷格、B.A.W.羅素和A.N.懷特海等加以發展和完善。現代數理邏輯的研究已遠遠超出了邏輯演算的範圍而發展成為四個主要分支──模型論、公理集合論、遞歸論和證明論。

由於形式推理在公理化數學中用得最多，表達得也最精確，因此邏輯演算的主要內容就是數學公理系統的形式化。形式化了的公理系統稱為形式系統。一般説,形式系統是由它的語言、公理和推理規則三部分構成。

形式系統的語言一般採用人工語言。首先要規定語言的符號。符號的有窮序列（允許一個符號在序列中重複出現）稱為一個表達式。正如自然語言中並非所有字母的序列都是句子一樣，並非所有的表達式都有意義。人們希望指出有意義的那部分表達式，稱之為公式。但判別一個表達式是否為公式的標準，並不是根據它們的意義而是根據某些確定的形式規則，因此稱之為形成規則。形成規則表明，語言中的符號依什麼樣的規律排列才形成公式，即語言中某一符號的序列是否為公式是可以依照形成規則機械地檢查的。形式系統的語言也稱為形式語言。

形式系統中的公理需滿足的惟一條件是它是該系統語言中的一個公式。推理規則（簡稱規則）陳述如何由有窮個確定的公式（稱為規則的假設）得到某一確定的公式(稱為規則的結論)。公理和推理規則一經確定，系統的全部定理就完全確定了。因為系統的定理通常是這樣定義的：①所有公理是定理；②若形式系統推理規則的假設都是定理，則它的結論也是定理。因此，形式系統的一個公式是否是它的定理也是可以機械地檢查的。

由以上説明可知，一個形式系統是由它的符號、表達式及其排列規則等完全確定了的。雖然每個形式系統都有邏輯推理系統或數學公理系統作為它的背景，即形式系統可以被解釋為邏輯推理或某個數學結構，但是形式系統的解釋或意義並不被認為是形式系統的一部分。這就使得形式系統本身成為一個純語法的對象。把公理、定理等作為形式語言中的公式、句子研究，稱為公理系統的語法研究。

形式系統的解釋或意義稱為語義。例如形式系統中的公式或句子在某個數學結構或模型中的真假性就是一個語義性質。

在數理邏輯中，建立形式系統的主要目的在於將通常所説的“形式的”思維、公理系統的“形式化”等概念精確化，使得數學中的語言、推理與數、形、方程式等一樣成為數學研究的對象。對形式系統可以進行嚴格的數學處理，討論其性質，包括語法與語義的性質，得出關於形式系統的一般結論。例如勒文海姆－斯科朗定理(見模型論)。哥德爾完備性定理（見一階邏輯）及哥德爾不完備性定理等都是關於形式系統性質的定理。又如希爾伯特第 1問題即連續統假設問題的研究就是在集合論公理系統形式化的基礎上才廓清了問題，並取得了進展。因此，數理邏輯中對形式系統的研究也給數學研究開闢了新的途徑。

那種認為建立邏輯演算的形式系統是為了進行形式思維，或者為了形式地證明數學定理的想法，是對於數理邏輯的研究對象和目的的一種誤解。

另一方面，數理邏輯中形式化的概念和方法對於編制計算機程序、建立計算機語言以及試圖系統地用計算機證明定理也是有用的。

對於不同類型的推理可以構造不同的邏輯演算的形式系統,其中主要有命題邏輯、一階邏輯、高階邏輯、模態邏輯、構造邏輯和無窮邏輯等。