等式邏輯

等式邏輯的 項 由變數和常數構成，使用函式符號（或運算）。形如以下的恆等式（等式）

(1)

其中 和 是項，構成了等式邏輯的 形式語言。等式邏輯的 三段論 總結如下。

1. 自反性

(2)

2. 對稱性

(3)

3. 傳遞性

(4)

4. 對於 函式符號和 ,

(5)

5. 對於 替換 (參見 合一),

(6)

上述規則說明，如果線上方的公式是透過應用 三段論 從公理形式推匯出的定理，則線下方的公式也是一個形式定理。通常，一些有限的恆等式集合 被作為 公理模式 給出。

等式邏輯可以與 一階邏輯 結合使用。在這種情況下，第四條規則也擴充套件到謂詞符號，第五條規則被省略。這些 三段論 可以轉化為具有 蘊含 形式的 公理模式，可以應用 肯定前件律。 一階邏輯 的主要結果在這種擴充套件理論中仍然成立。

如果將 中的每個恆等式視為兩個重寫規則，將左側轉換為右側，反之亦然，則相應的 項重寫系統 等價於由 定義的等式邏輯：恆等式 在等式邏輯中是 可推導的，當且僅當 在 項重寫系統 中。此屬性稱為 項重寫系統 的邏輯性。

等式邏輯是完備的，因為如果代數 是 的模型，即來自 的所有恆等式在代數 中成立（參見 泛代數），那麼 在 中成立，當且僅當 它可以在由 定義的等式邏輯中推匯出來。這個定理有時被稱為伯克霍夫定理。