一阶逻辑

一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。

高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。

在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）的。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯（英语：Metalogic）定理，如勒文海姆–斯科倫定理及緊緻性定理。

一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種“病態”集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象。

簡介

基本符號

命題邏輯顧名思義，會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假的敘述簡記為 $p$ 及 $q$ （也就是有真有假的命題），然後討論 $\neg p$ （非p）、 $p\Rightarrow q$ （若p則q）、 $p\wedge q$ （p且q）與 $p\vee q$ （p或q）之間的推理關係。

但一階邏輯嘗試從一些比較基礎的詞彙去建構「句子」，比如說，可用符號 ${\text{Phil}}(x)$ 代表「 x 是哲學家」，也就是賦予斷言符號「 ${\text{Phil}}(x)$ 」語意的解釋。這個解釋預設一個「所有人類的群體」（也就是下面標準語義一節會說到的论域），并將變數 $x$ 對應為自群體中取出來的某人。

以此類推，斷言符號可以包含一個以上的變數。例如：可以將 ${\text{Cp}}(x,\,y)$ 解釋為「 x 與 y 是夫妻」。

一階邏輯類似於命題邏輯，可以將斷言符號與 $\neg$ （非）、 $\Rightarrow$ （則）、 $\wedge$ （且）和 $\vee$ （或）組成更複雜的敘述，例如：把斷言符號 ${\text{Schol}}(x)$ 解釋成「 $x$ 是學者」，那「若 x 為哲學家，則 x 為學者」可表示為：

{\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)\,

但相較之下，一階邏輯又加入了描述「所有」與「存在」的量詞，比如說「對所有 x ，若 x 為哲學家，則 x 為學者」可記為：

\forall x[{\text{Phil}}(x)\Rightarrow {\text{Schol}}(x)]

也就是自左方開始閱讀，將 $\forall x$ 解釋成「对所有 x 有…」。 $\forall$ 這個符號被称为全稱量詞。

而對於「有 x 是哲學家」这一叙述，一階邏輯則引入另一種量詞：

\exists x[{\text{Phil}}(x)]

也就是自左方開始閱讀，將 $\exists x$ 解釋成「存在 $x$ 使…」。 $\exists$ 這個符號被称为存在量詞。

順帶一提「並非所有 x 不是哲學家」等價於「有 x 是哲學家」；且「不存在 x 不是學者」也等價於「所有的 x 是學者」。所以可以用「否定」和「全稱量詞」來組合出「存在量詞」。換句話說，可作以下的符號定義（ ${\mathcal {A}}$ 代表一段「敘述」）：

\exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]

相等

一階邏輯也考慮到「相等」這個概念在敘述中的重要性，例如想表達「若所有 $x$ 是哲學家，那 $x$ 的長子也會是哲學家」，可先把 ${\text{Son}}(x)$ 解釋為「 x 的長子」，那么這段敘述可記為：

\forall x{\text{Phil}}(x)\Rightarrow {\text{Phil}}[{\text{Son}}(x)]

換句話說， ${\text{Son}}(x)$ 被解釋成「與 $x$ 有特定且唯一對應關係」的某對象（被稱為函數符號）。換句話話說，只要「 $x$ 就是 $y$ 」，那「 $x$ 的長子也會是 $y$ 的長子」。換句話說：

(x=y)\Rightarrow [{\text{Son}}(x)={\text{Son}}(y)]

這些性質被一階邏輯視為「理所當然」。

類似地，敘述中也有一些「不變的實體」，如苏格拉底，表示這些「實體」的符號被稱為常數符號。例如將 $s$ 解釋為苏格拉底，那「苏格拉底為哲學家」就可以寫成：

{\text{Phil}}(s)

所謂的「不變」隱含的代表：

「蘇格拉底就是蘇格拉底」

「對所有x，對所有y，如果x就是蘇格拉底，且y就是蘇格拉底，那x就是y」

換句話說

(s=s)

\forall x\forall y\{[(x=s)\wedge (y=s)]\Rightarrow (x=y)\}

這兩個性質也被一階邏輯視為「理所當然」。

形式理論

一階邏輯的形式理論可分成幾個部份：

語法（英语：Syntax (logic)）：決定哪些符號組合是合式公式。（直觀上的“文法無誤的敘述”）
推理規則：由合式公式符號組合出新合式公式的規則（直觀上的“推理”）
公理：一套合式公式（直觀上的基本假設）

基本符號

一套理論能容許多少符號，取決於人類能運用物理定律來塑造多少符號，但目前無法確知宇宙是不是有限，或是以可無限制地分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認跟自然數一樣多的無窮（如ZF集合論的無窮公理），甚至以這樣的可數無窮為基礎，去建構出不可數的實數，但將抽象的理論對應到現實時，還是需要回答物理上有沒有可數或不可數的無窮。所以謹慎起見，如果沒有特別申明的話，以下各種類符號的數目上限都是有限的。

邏輯符號

一階邏輯通常擁有以下的符號：

量化符號 $\forall$ 及 $\exists$
- 某些作者會把 $\exists$ 符號定義為 $\exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]$ ，如此便只需要 $\forall$ 做為基礎符號。
邏輯聯結詞：以下為可能的表示符號（关于波蘭表示法下的邏輯連接詞，請參見逻辑运算的波兰记法）：
- 否定： $\neg$ 或 $\sim$ 或－
- 條件： $\Rightarrow$ 或 $\rightarrow$ 或 $\supset$
- 且： $\land$ 或 $\&$
- 或： $\lor$ 或 ||
- 雙條件： $\Leftrightarrow$ 或 $\leftrightarrow$
- 某些作者會作如下的符號定義：
${\mathcal {A}}\wedge {\mathcal {B}}:=\neg ({\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})),$

${\mathcal {A}}\vee {\mathcal {B}}:=(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}},$

${\mathcal {A}}\Leftrightarrow {\mathcal {B}}:=({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}}),$

如此一來只需要否定和條件做為基礎符號。
標點符號：括號、逗號及其他，依作者的喜好有所不同。
- 為了更有效的將括號做配對，通常還會採用大括號{ }跟中括號[ ]。
至多跟自然數一樣多的變數，通常標記為英文字母末端的小寫字母x、y、z、…，也常會使用下標（或上標、上下標兼有）來區別不同的變數：x₀、x₁、x₂、…（特別注意c有時候會被當成常數符號而引起混淆）。
等式符號： $=$
- 有作者會因為語義上对“相等”的不同解释，而將等式符號視為雙元斷言符號、甚至是某種合式公式的簡寫。
符號相等： $\asymp$
- 某些作者會額外採用這個符號來表示符號辨識上的等同以便與等式符號作區別。

並非所有的符號都不可或缺的，像謝費爾豎線「 $|$ 」（或異或）可以用來定義量詞以外的所有邏輯符號，換句話說：

符號定義 —
$(\neg {\mathcal {A}}):=({\mathcal {A}}|{\mathcal {A}})$

$({\mathcal {A}}\Rightarrow {\mathcal {B}}):={\mathcal {A}}|({\mathcal {B}}|{\mathcal {B}})$

$({\mathcal {A}}\wedge {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {B}})|({\mathcal {A}}|{\mathcal {B}})\,]$

$({\mathcal {A}}\vee {\mathcal {B}}):=[\,({\mathcal {A}}|{\mathcal {A}})|({\mathcal {B}}|{\mathcal {B}})\,]$

另外，一些作者不區分語義解釋和形式理論，所以會將表示真值的符號納入形式理論裡，也就是說，用 T 、Vpq 或 $\top$ 來表示「真」，並用 F 、 Opq 或 $\bot$ 來表示「假」。

斷言符號

「他們兩人是夫妻」，是一個關於兩個“對象”的斷言，而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數 $n$ 、 $j$ 約定：

A_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})

為一階邏輯的合法詞彙。它在直觀上表示一個有 $n$ 個“對象”的斷言，稱為 $n$ 元斷言符號。下標的自然數 $j$ 只是拿來和其他同為 $n$ 元的斷言符號作區別。

實用上只要有申明，不至於和其他詞彙引起混淆的話，可以用任意的形式簡寫一個斷言符號。如：公理化集合論裡的雙元斷言符號 $A_{1}^{2}(x,\,y)$ 也可以表示为 $x\in y$ 。

函數符號

「物體的顏色」、「夫妻的長子」这种断言說明了一组對象所唯一對應的對象。但不同的夫妻有不同的長子；不同的物體有不同的顏色。據此，形式上對於自然數 $n$ 、 $j$ 約定：

f_{j}^{n}(x_{1},\,x_{2},\,...,\,x_{n})

為一階邏輯的合法詞彙，直觀上表示 $n$ 個“對象”所對應到的東西，稱它為 $n$ 元函數符號。需要特別注意，這種“唯一對應”的直觀想法，必須配上關於“等式”的性質（詳見下面的等式定理章节），才能在形式理論中被實現。

与斷言符號一样，只要不引起混淆，就可以用任何的形式簡寫函數符號。如：公理化集合論裡的 $x\cup y$ 是依據聯集公理而定義的新函數符號（請參見下面函數符號與唯一性章節），也可以冗長的表記為 $f_{j}^{2}(x,\,y)$ 。

常數符號

「刻度0」、「原點」、「蘇格拉底」是直觀上＂唯一不變＂的對象。據此，對自然數 $j$ 約定

c_{j}

為一階邏輯的合法詞彙，直觀上表示一個“唯一不變”的對象，稱為常數符號。同樣的。“常數的不變性”需配上等式的性質（詳見下面等式定理）才能被實現。

為了不和變數的表記混淆，常數符號一樣可以用任何的形式簡寫，如公理化集合論裡的 $\varnothing$ 是根據空集公理和函數符號與唯一性，而定義的新常數符號。亦可冗長的表示為 $c_{j}$ 。

語法

和自然語言（如英語）不同，一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說，一階邏輯以「項」代表討論的對象，而對「項」的斷言組成了最基本的原子（合式）公式；而原子公式和邏輯符號組成了更複雜的合式公式（也就是“敘述”）。

項

「那對夫妻的長子的職業」、「 $(x+y)\times z$ 」、「 $x\cup \varnothing$ 」代表變數可以與函數符號組成更一般的物件。據此形式，遞迴地規定一類合法詞彙——項為：

遞迴定義 —

變數和常數是項。
若 $T_{1},\,....,\,T_{n}$ 全都是項，那么 $f_{j}^{n}(T_{1},\,....,\,T_{n})$ 也是項。
項只能通过以上兩點，於有限步驟內建構出來。

習慣上以大寫的西方字母（如英文字母、希伯來字母、希臘字母）代表項，如果變數不得不採用大寫字母，而可能跟項引起混淆的話，需額外規定分辨的辦法。

原子公式

為了比較簡潔地規定甚麼是合式公式，先規定原子公式為：（若 $T_{1},\,....,\,T_{n}$ 是項）

A_{j}^{n}(T_{1},\,....,\,T_{n})

這樣的形式。

公式

一階邏輯的合式公式（簡稱公式或 $wf$ ）以下面的規則遞迴地定義：

遞迴定義 —

原子公式為公式。（美觀起見，在原子公式外面包一層括弧也是公式）
若 ${\mathcal {A}}$ 為公式，則 $(\neg {\mathcal {A}})$ 為公式。
若 ${\mathcal {A}}$ 與 ${\mathcal {B}}$ 為公式，則 $({\mathcal {A}}\Rightarrow {\mathcal {B}})$ 為公式。
若 ${\mathcal {A}}$ 為公式， $x$ 為任意變數，則 $(\forall x{\mathcal {A}})$ 為公式。（美觀起見 $(\forall x){\mathcal {A}}:=\forall x{\mathcal {A}}$ ，也就是裡面的量詞有無外包括弧都是公式）
合式公式只能通过以上四點，於有限步驟內建構出來。

另外成對的中括弧跟大括弧，符號辨識上視為成對的小括弧，而草書的大寫西方字母為公式的代號。

舉例來說，

\{(\forall y)A_{1}^{2}[x,\,f_{1}^{1}(y)]\}

是公式而

\forall x\,x\Rightarrow

則不是公式。

而接下來只要對任意公式 ${\mathcal {A}}$ 、 ${\mathcal {B}}$ 與變數 $x$ ，做以下符號定義

符號定義 —
$({\mathcal {A}}\wedge {\mathcal {B}}):=\{\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]\}$

$({\mathcal {A}}\vee {\mathcal {B}}):=[(\neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]$

$({\mathcal {A}}\Leftrightarrow {\mathcal {B}}):=[({\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge ({\mathcal {B}}\Rightarrow {\mathcal {A}})]$

$(\exists x{\mathcal {A}}):=\{\neg [\forall x(\neg {\mathcal {A}})]\}$ （同樣美觀起見 $(\exists x){\mathcal {A}}:=\exists x{\mathcal {A}}$ ）

這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。

施用

所謂的施用/作用，是以下公式形式的口語說法：（其中 ${\mathcal {A}}$ 與 ${\mathcal {B}}$ 都是公式）

$(\neg {\mathcal {A}})$ 稱為 $\neg$ 施用於 ${\mathcal {A}}$ 上。
$({\mathcal {A}}\Rightarrow {\mathcal {B}})$ 稱為 $\Rightarrow$ 施用於 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
$({\mathcal {A}}\wedge {\mathcal {B}})$ 稱為 $\wedge$ 施用於 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
$({\mathcal {A}}\vee {\mathcal {B}})$ 稱為 $\vee$ 施用於 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
$({\mathcal {A}}\Leftrightarrow {\mathcal {B}})$ 稱為 $\Leftrightarrow$ 施用於 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 上。
$(\forall x{\mathcal {A}})$ 稱為 $\forall x$ 施用於 ${\mathcal {A}}$ 上。
$(\exists x{\mathcal {A}})$ 稱為 $\exists x$ 施用於 ${\mathcal {A}}$ 上。

就类似于運算子作用在它們身上。

自由變數和約束變數

量詞所施用的公式被稱為量詞的範圍（scope）。同一個變數在公式一般來說不只出現一次，若變數 $x$ 出現在 $\forall x$ 的範圍內，稱這樣出現的 $x$ 為不自由/被約束的 $x$ （not free/bounded）；反過來說，不出現在 $\forall x$ 的範圍內的某個 $x$ 被稱為自由的 $x$ 。

例如，對於公式：

\{(\forall x)[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]\}

$[A_{1}^{1}(x)\Rightarrow A_{2}^{1}(y)]$ 就是量詞 $\forall x$ 的範圍；而 $A_{1}^{1}(x)$ 裡的 $x$ 就是不自由的；反之 $A_{2}^{1}(y)$ 裡的 $y$ 就是自由的。

說 $x$ 於公式 ${\mathcal {A}}$ 完全自由，意為於 ${\mathcal {A}}$ 出現的 $x$ 都是自由的；反之，說 $x$ 於公式 ${\mathcal {A}}$ 完全不自由/完全被約束，意為 ${\mathcal {A}}$ 內根本沒有 $x$ ，或是 ${\mathcal {A}}$ 內沒有自由的 $x$ 。若 ${\mathcal {A}}$ 內所有的變數都完全不自由， ${\mathcal {A}}$ 特稱為封閉公式/句子（closed formula/sentence）。

括弧的簡寫

括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此規定以下的“重構法”（反過來就是“簡寫法”），從表面上不合法的一串符號找出作者原來想表達的公式：

若整串符號的括弧不成對，直接視為無法重構。
以 $\lnot ,\,\land ,\,\lor ,\,\forall ,\,\exists ,\,\Rightarrow ,\,\Leftrightarrow$ （左至右）的施用順序重構括弧。
相鄰的邏輯連接詞或量詞無法決定施用順序的話，以右邊為先。
重構施用的順序，以被成對括弧包住的部分為優先施用，其次才是落單的斷言符號。

舉例來說

\lnot [\forall xA_{1}^{1}(x)]\Rightarrow \exists x\lnot A_{2}^{1}(x)

的重構過程如下

$\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)]$ （優先施用 $\lnot$ ）
$\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}$ （施用 $\exists$ ）
$\{\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}\}$ （最後施用 $\Rightarrow$ ）

可以被重構為公式的一串符號則寬鬆的認定為“合式公式”。（最明顯的例子就是合式公式最外層的括弧可以省略）

波蘭表示法

波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間。如果沿用以上的＂施用順序＂，這個表示法允許捨棄所有括弧。如公式

\forall x\forall y\{A_{1}^{1}[f_{1}^{1}(x)]\Rightarrow \neg \{A_{1}^{1}(x)\Rightarrow A_{1}^{3}[f_{1}^{1}(y),x,z]\}\}

轉成波蘭表示法的過程如下

\forall x\forall y\Rightarrow A_{1}^{1}f_{1}^{1}x\neg \Rightarrow A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz

（轉成波蘭表示法的順序）

\Pi x\Pi y{\text{C}}A_{1}^{1}f_{1}^{1}x{\text{N}}{\text{C}}A_{1}^{1}xA_{1}^{3}f_{1}^{1}yxz

（邏輯連結詞的符號轉換）

推理规则

一階邏輯通常只有以下的推理規則（因為將普遍化視為推理規則會有不直觀的限制）

MP律 — 對於公式 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 有

{\mathcal {A}}\Rightarrow {\mathcal {B}}

和

{\mathcal {A}}

組合出

{\mathcal {B}}

。

直觀意義非常明顯，就是p=>q且p可以推出q。

在只以謝費爾豎線「 $|$ 」為基礎邏輯連接詞的公理系统裡，MP律會被改寫成

修改的MP律 — 對於公式 ${\mathcal {A}}$ 、 ${\mathcal {B}}$ 和 ${\mathcal {C}}$ 有 ${\mathcal {A}}|({\mathcal {C}}|{\mathcal {B}})$ 和 ${\mathcal {A}}$ 組合出 ${\mathcal {B}}$ 。

公理

邏輯公理

公理 — 如果 ${\mathcal {B}}$ 、 ${\mathcal {C}}$ 、 ${\mathcal {D}}$ 都是公式，則：

（A1） ${\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})$
（A2） $[{\mathcal {B}}\Rightarrow ({\mathcal {C}}\Rightarrow {\mathcal {D}})]\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {D}})]$
（A3） $[(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})]\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {C}})\Rightarrow {\mathcal {B}}]$

都是公理。

它们实际上是公理模式，代表著“跟自然數一樣多”條的公理。

在有（A1）與（A2）的前提下，（A3）等價於以下的公理模式：（證明請參見下面否定一節。）

（T1） — $[\,(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})\,]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$

另外，在只以謝費爾豎線「 $|$ 」為基礎邏輯連接詞的公理系统裡，上面三條公理模式等價於下面這條公理模式：

公理 — 如果 ${\mathcal {B}}$ 、 ${\mathcal {C}}$ 、 ${\mathcal {D}}$ 、 ${\mathcal {E}}$ 和 ${\mathcal {F}}$ 都是公式，則：

$[\,{\mathcal {B}}|({\mathcal {C}}|{\mathcal {D}})\,]|{\big \{}\,[\,{\mathcal {E}}|({\mathcal {E}}|{\mathcal {E}})\,]|\{\,({\mathcal {F}}|{\mathcal {C}})|[\,({\mathcal {B}}|{\mathcal {F}})|({\mathcal {B}}|{\mathcal {F}})\,]\,\}\,{\big \}}$

都是公理。

量词公理

公理 — $x$ 為任意變數， ${\mathcal {B}}$ 、 ${\mathcal {C}}$ 為任意公式，則

（A4） $T$ 是一個項， $t$ 為 $T$ 中出現的任意變數；若 ${\mathcal {B}}$ 裡，自由的 $x$ 都不在 $\forall t$ 的範圍裡（這樣取代成 $T$ 時才不會被 $\forall t$ 約束），則

(\forall x){\mathcal {B}}\Rightarrow {\mathcal {B}}(T)

為公理

其中

{\mathcal {B}}(T)

代表把

{\mathcal {B}}

裡自由的

x

都替換成

T

所得到的新公式。

（A5）如果 $x$ 在 ${\mathcal {B}}$ 裡完全被約束，則

[(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [{\mathcal {B}}\Rightarrow (\forall x{\mathcal {C}})]

為公理

（A6） $[(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Rightarrow [(\forall x{\mathcal {B}})\Rightarrow (\forall x{\mathcal {C}})]$ 為公理
（A7）若 ${\mathcal {B}}$ 是公理， $x$ 是任意變數，則

(\forall x){\mathcal {B}}

也是公理。

它们实际上也是公理模式。

等式和它的公理

根據不同作者的看法，甚至是理論本身的需求，「等式」在形式理論裡可能是斷言符號或是一段公式（如 a 等於 b 可定義為對所有的 x ， x 屬於 a 等價於 x 屬於 b ）。而如何刻劃直觀上「等式的性質」，有一開始就將「等式的性質」視為公理（模式），但也有視為元定理的另一套處理方法，以下暫且以公理模式的方式處理。以元定理處理的方法會在等式定理詳述。

公理 — $(x=y)$ 是一段變數 $x$ 、 $y$ 完全自由，且型式完全被確定的公式 ${\mathcal {E}}(x,\,y)$ 的簡寫。要求：

（E1） $(\forall x)(x=x)$ 為公理。
（E2）若在公式 ${\mathcal {A}}$ 中自由的 $x$ 都不在 $\forall y$ 的範圍內，以 ${\mathcal {A}}_{y}$ 代表 ${\mathcal {A}}$ 某些（而非全部）自由的 $x$ 被取代成 $y$ 而成的新公式，則

(\forall x)(\forall y)[(x=y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})]

為公理。

事實上這兩個公理模式也確保了函數符號“唯一對應”和常數符號的“唯一性”，但證明這些性質需要一些元定理，簡便起見合併於下面的等式定理一節講述。

標準語義

一階邏輯的標準語義源於波蘭邏輯學家阿尔弗雷德·塔斯基所著《On the Concept of Truth in Formal Languages》。根據上面語法一節，公式是由原子公式遞迴地添加邏輯連結詞而來的，而原子公式是由斷言符號與項所構成的。所以要檢驗一條公式在特定的論域下正不正確，就要規定項的取值，然後檢驗這樣的取值會不會落在斷言符號所對應的關係裡。由此延伸出所有公式的“真假值”。

也就是一套一階邏輯的語義解釋，要包含

變數取值的論域
如何解釋函數符號（為論域中的某個函數）與常數符號（為論域中的某特定元素），以便從特定的變數取值得出項的取值。
如何將斷言符號與論域裡的某關係做對應。

通常一套解釋方法（簡稱為解釋）會以代號 $M$ 表示。

項的取值

量詞的解釋需要指明變數取值範圍的論域——也就是一個集合 $D$ 。而變數可能跟自然數一樣多，換句話說，所有變數在論域 $D$ 取的值可以依序以自然數標下標——也就是一個在 $D$ 取值的數列。如果以 $x_{1},\,x_{2},\,x_{3},\,\cdots$ 的代號（不一定是變數本身的表示符號）來列舉變數，那麼從 $D$ 的某套變數取值就以

\left\langle a_{k}\right\rangle _{k\in \mathbb {N} }

或較直觀的符號

\left\langle a_{1},\,a_{2},\,a_{3},\,\cdots \right\rangle

來表示。

一套解釋 $M$ 會將 $n$ 元函數符號 $f_{i}^{n}$ 解釋成某個 ${(f_{i}^{n})}^{M}:D^{n}\to D$ 的 $n$ 元函數；而常數符號 $c_{l}$ 解釋成特定的 ${c_{l}}^{M}\in D$ （亦稱為 $c_{l}$ 的取值為 ${c_{l}}^{M}$ ），這樣就可以用上面語法一節定義項的方式，遞迴地規定項的取值：

元定義 — 在解釋 $M$ 下的某套變數取值下，一列項 $T_{1},\,\cdots ,\,T_{n}$ 的取值分別為 ${T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M}$ ，則這套變數取值下，項 $f_{i}^{n}(T_{1},\,\cdots ,\,T_{n})$ 的取值規定為

{(f_{i}^{n})}^{M}({T_{1}}^{M},\,\cdots ,\,{T_{n}}^{M})

真假的賦值

直觀上要解釋關係最直接的方法，就是列舉所有符合關係的對象；例如如果想說明夫妻關係，可以列舉所有（老公, 老婆）的雙元有序對，但並非所有的人類有序對都會在這個關係中。

以此為基礎，若以 $D^{m}$ 代表所有以 $m$ 個 $D$ 中的元素構成的 $m$ 元有序對的集合（也就是 $m$ 元笛卡兒積），那一套解釋 $M$ 會將 $m$ 元斷言符號 $A_{j}^{m}$ 解釋為一個

{(A_{j}^{m})}^{M}\subseteq D^{m}

的 $m$ 元有序對子集合。

這樣就可以依據語法的遞迴定義，以下面的規則對每條公式賦予真值。（這種賦值方式稱為T-模式，取名於邏輯學家阿尔弗雷德·塔斯基）

元定義 — 在一套解釋 $M$ 下：

在一套特定的變數取值下，一列項 $T_{1},\,\cdots ,\,T_{m}$ 的取值為 ${T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M}$ ，那 $A_{j}^{m}(T_{1},\,\cdots ,\,T_{m})$ 為真定義為

({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\in {(A_{j}^{m})}^{M}

反之

({T_{1}}^{M},\,\cdots ,\,{T_{m}}^{M})\notin {(A_{j}^{m})}^{M}

則定義為假。

在一套特定的變數取值下，「 $(\neg {\mathcal {B}})$ 為真」等價於「 ${\mathcal {B}}$ 為假」。
在一套特定的變數取值下， $({\mathcal {B}}\Rightarrow {\mathcal {C}})$ 為真，意為「 ${\mathcal {B}}$ 為假或是 ${\mathcal {C}}$ 為真。」（p=>q為假只有p為真且q為假的狀況）
在變數取值 $\left\langle a_{k}\right\rangle _{k\in \mathbb {N} }$ 下， $(\forall x_{i}{\mathcal {B}})$ 為真，意為「對所有的 $d\in D$ ， ${\mathcal {B}}$ 於變數取值 $\left\langle a_{1},\,\cdots ,\,a_{i-1},\,d,\,a_{i+1},\,\cdots \right\rangle$ 下為真」。（也就是把變數 $x_{i}$ 的取值換為論域的任意元素仍然為真）

更進一步的來說

元定義 — #在一套解釋 $M$ 下，不管怎麼樣的變數取值，公式 ${\mathcal {B}}$ 都為真，則稱為 $M$ 下 ${\mathcal {B}}$ 為真，以符號 $M\vDash {\mathcal {B}}$ 簡記。若沒有變數取值可以滿足 ${\mathcal {B}}$ ，則稱 $M$ 下 ${\mathcal {B}}$ 為假。

若任意解釋下公式 ${\mathcal {B}}$ 都為真，稱 ${\mathcal {B}}$ 為邏輯有效的（logically valid）（類似於命題邏輯的恆真式）
若一階邏輯理論 ${\mathcal {L}}$ 的公理都於 $M$ 為真，稱解釋 $M$ 為 ${\mathcal {L}}$ 之模型（model）

代數化語義

另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型：

圓柱代數，由阿爾弗雷德·塔斯基和其同事提出；
多元代數，由保羅·哈爾莫斯提出。
斷言函子邏輯，主要是基於威拉德·范·奧曼·奎因的工作成果。

這些代數都是純粹擴展兩元素布林代數而成的格。

塔斯基和葛范德於1987年證明，沒有超過包在三個以上的量化內的原子句子的部份一階邏輯，其表示力和關係代數相同。上述部份一階邏輯令人十分地感到有興趣，因為它已足夠表示皮亞諾算術和公理化集合論，包括典型的ZFC。他們亦證明了，具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價。

空論域

上述的語義解釋都要求論域為非空集合。但在如自由邏輯之中，設定空論域是被允許的。甚至代數結構的類包含一個空結構（如空偏序集），當允許空論域時，這個類只能是一階邏輯中的一個基本類，不然就要將空結構由類中移除。

不過，空論域存在著一些難點：

許多常見的推理規則只在論域被要求是非空時才為有效的。一個例子為，當x不是 $\phi \,$ 內的自由變數時， $\phi \lor \exists x\psi$ 會薀涵 $\exists x(\phi \lor \psi )$ 。這個用來將公式寫成前束範式的規則在非空論域中是可靠的，但在允許空論域時則是不可靠的。
在使用變數賦值函數的解釋中，真值的定義不能和空論域一起運作，因為不存在範圍為空的變數賦值函數。（相似地，也無法將解釋賦予上常數符號。）在甚至是原子公式的真值可被定義之前，都必須選定一個變數賦值函數。然後一個句子的真值即可在任一個變數賦值之下定義出其真值，且可證明其真值不依選定的賦值而變。這個做法在賦值函數不存在時不能運作；除非將其改成配上空論域。

因此，若空論域是被允許的，通常也必須被視成特例。不過，大多數的作家會簡單地將空論域由定義中排除。

常用的推理性質

定理與證明

以下介紹一些基本用語和符號

元定義 — 在一階邏輯理論 ${\mathcal {L}}$ 下， $\vdash _{\mathcal {L}}{\mathcal {A}}$ 代表有一列公式 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 滿足：

${\mathcal {C}}_{n}$ 符號辨識上為 ${\mathcal {A}}$ 。
所有的 ${\mathcal {C}}_{k}$ 有下列兩種可能情況

${\mathcal {C}}_{k}$ 為 ${\mathcal {L}}$ 的公理。
存在 $i,\,j<k$ 使得 ${\mathcal {C}}_{i}$ 為 $({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k})$ （也就是由前面的公式以MP律組合出來）

口語上會稱公式 ${\mathcal {A}}$ （或 $\vdash _{\mathcal {L}}{\mathcal {A}}$ ）為 ${\mathcal {L}}$ 下的定理（theorem）。而這列 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 會稱為 $\vdash _{\mathcal {L}}{\mathcal {A}}$ 的證明。

例如定理 $(I)$ $\vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {B}}$ 的證明：

證明 —

{\mathcal {C}}_{1}

：

\{{\mathcal {B}}\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\}\Rightarrow \{[{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})\}

（公理A2）

{\mathcal {C}}_{2}

：

{\mathcal {B}}\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]

（公理A1）

{\mathcal {C}}_{3}

：

{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})

（公理A1）

{\mathcal {C}}_{4}

：

[{\mathcal {B}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})]\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {B}})

（

{\mathcal {C}}_{1}

和

{\mathcal {C}}_{2}

加上MP律）

{\mathcal {C}}_{5}

：

{\mathcal {B}}\Rightarrow {\mathcal {B}}

（

{\mathcal {C}}_{4}

和

{\mathcal {C}}_{3}

加上MP律）

以上其實是蘊含了無限多定理的元定理的證明(因為沒有給出合式公式的明確形式)。方便起見，這種元定理還是會稱為定理並以同樣的形式來表達。

直觀上的證明，總是會有一些“前提假設”，對此，若以 $\Gamma$ 代表一列有限數目的公式，那

元定義 — $\Gamma \vdash _{\mathcal {L}}{\mathcal {A}}$ 代表有一列公式 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 滿足：

${\mathcal {C}}_{n}$ 符號辨識上為 ${\mathcal {A}}$ 。
所有的 ${\mathcal {C}}_{k}$ 有下列三種可能情況

${\mathcal {C}}_{k}$ 為 ${\mathcal {L}}$ 的公理。
${\mathcal {C}}_{k}$ 為 $\Gamma$ 中的其中一條公式。
存在 $i,\,j<k$ 使得 ${\mathcal {C}}_{i}$ 為 $({\mathcal {C}}_{j}\Rightarrow {\mathcal {C}}_{k})$ （也就是由前面的公式以MP律組合出來）

這樣稱 ${\mathcal {C}}_{i}\,\,(1\leq i\leq n)$ 為在前提 $\Gamma$ 下， ${\mathcal {A}}$ 的證明；或是說 ${\mathcal {A}}$ 是 $\Gamma$ 的推論結果。

若要特別凸顯 $\Gamma$ 裡的一條＂前提條件＂ ${\mathcal {B}}$ 對＂證明過程＂的重要性，可以用 $\Gamma ,\,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {A}}$ 的符號去特別凸顯。若 $\Gamma$ 裡的公式列舉出來有 ${\mathcal {B}}_{1},...,{\mathcal {B}}_{n}$ ，那亦可表示為

{\mathcal {B}}_{1},...,{\mathcal {B}}_{n}\vdash _{\mathcal {L}}{\mathcal {A}}

證明過程沒有被引用的公式盡可能不寫出來。另一方面從以上對於證明定義可以發現，依怎樣的順序列舉前提條件，對於證明本身是不會有任何影響的。

本節所介紹的符號，在引用哪個理論很顯然的情況下， $\vdash _{\mathcal {L}}$ 的下標 ${\mathcal {L}}$ 可以省略。

實際的證明常常會＂引用＂別的（元）定理，嚴格來說，就是照抄（元）定理的證明過程，然後作一些修改使符號一致。為了節省證明的篇幅，引用時只會單單列出配合引用（元）定理所得出的公式（形式），並在後面註明引用的（元）定理代號。

演繹元定理

從公理（A1）和（A2）會得出不但直觀且實用的演繹元定理：

元定理 —
一階邏輯理論 ${\mathcal {L}}$ 下，若有 $\Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}$ ，則有 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}$

證明
（注意這是元邏輯（英语：Metalogic）下的證明）：假設 ${\mathcal {C}}_{1},{\mathcal {C}}_{2},....,{\mathcal {C}}_{n}$ 為條件所說 ${\mathcal {C}}$ 的證明，如果 ${\mathcal {C}}_{1}$ 是 $\Gamma$ 裡的公式或 ${\mathcal {L}}$ 的公理，那根據（A1） $\vdash {\mathcal {C}}_{1}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}_{1})$ 所以由MP律有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{1}$ 若 ${\mathcal {C}}_{1}$ 是 ${\mathcal {B}}$ ，那因為 $\vdash {\mathcal {B}}\Rightarrow {\mathcal {B}}$ 所以有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{1}$ 至此 ${\mathcal {C}}_{1}$ 的部分證明完畢。接下來要用歸納法；假設對 $i<k$ 都有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{i}$ 。若 ${\mathcal {C}}_{k}$ 是公理、或從 $\Gamma$ 來的、或是根本就是 ${\mathcal {B}}$ ，仿造上面 ${\mathcal {C}}_{1}$ 的部分就有 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{k}$ 剩下沒考慮的狀況是由MP律組合出 ${\mathcal {C}}_{k}$ 的狀況，也就是有 $l,m<k$ 使 ${\mathcal {C}}_{m}$ 是 ${\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k}$ 。由公理A2有 $\vdash [{\mathcal {B}}\Rightarrow ({\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k})]\Rightarrow [({\mathcal {B}}\Rightarrow {\mathcal {C}}_{l})\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}_{k})]$ 套用歸納法的假設，加上MP律，就會發現 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}_{k}$ 如此可以一路歸納到 ${\mathcal {C}}_{n}$ 也就是 ${\mathcal {C}}$ 的情況，故元定理得證。 $\Box$

因為 $\Gamma$ 代表的是有限條公式，所以透過演繹元定理可以將證明過程必要的前提條件遞迴地移到 $\vdash$ 後，直到不需要任何前提為止；然後由MP律可以知道，若有 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}\Rightarrow {\mathcal {C}}$ ，則有 $\Gamma ,{\mathcal {B}}\vdash _{\mathcal {L}}{\mathcal {C}}$ ，如此一來透過演繹元定理搬到推論結果的合式公式，也可以任意的搬回來。所以 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}$ 等價於某定理 $\vdash _{\mathcal {L}}{\mathcal {C}}$ 。因此也會將 $\Gamma \vdash _{\mathcal {L}}{\mathcal {B}}$ 稱為一個定理。

而從演繹元定理和MP律，會有以下直觀且實用的元定理

元定理 —
（D1） ${\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{2},\,{\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}$

（D2） ${\mathcal {D}}_{1}\Rightarrow ({\mathcal {D}}_{2}\Rightarrow {\mathcal {D}}_{3}),\,{\mathcal {D}}_{2}\vdash \,{\mathcal {D}}_{1}\Rightarrow {\mathcal {D}}_{3}$

以下如果需要將引用的定理以演繹元定理進行＂搬移＂，會省略掉搬移的過程並在搬移後得到的結果後標註（D）。如果引用以上的（D1）和（D2）也會省略過程，單有結果和代號標註。

否定

以下的證明會分成使用（A3）的部分跟將公理（A3）取代為（T1）的部分，用以證明兩者的等價性。

（DNe） Double negation, elimination —
$\vdash \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$

證明（使用A3）
（1） $(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}]$ （A3）（2） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （I）（3） $(\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow {\mathcal {A}}$ （D2 with 1, 2）（4） $\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1）（5） $\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

證明（使用T1）
（1） $\neg \neg {\mathcal {A}}\Rightarrow (\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}})$ （A1）（2） $\neg \neg {\mathcal {A}}$ （Hyp）（3） $\neg \neg \neg \neg {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 1）（4） $\neg {\mathcal {A}}\Rightarrow \neg \neg \neg {\mathcal {A}}$ （MP with 3, T1）（5） $\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （MP with 4, T1）（6） ${\mathcal {A}}$ （MP with 2, 5）

（DNi） Double negation, introduction —
$\vdash {\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$

證明（使用A3）
（1） $(\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}]$ （A3）（2） $(\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})\Rightarrow \neg \neg {\mathcal {A}}$ （MP with DNe, 1）（3） ${\mathcal {A}}\Rightarrow (\neg \neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}})$ （A1）（4） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 2,3）

證明（使用T1）
（1） $\neg \neg \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {A}}$ （DNe）（2） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 1, T1）

上面兩定理表達了雙否定推理上等價於於原公式，引用兩者任一會都以（DN）簡寫。

（T1） Transposition-1 —
$\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}\vdash {\mathcal {B}}\Rightarrow {\mathcal {A}}$

證明（使用A3）
（1） $(\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}]$ （A3）（2） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （Hyp）（3） $(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {A}}$ （MP with 1, 2）（4） ${\mathcal {B}}\Rightarrow (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （A1）（5） ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D1 with 3, 4）

（T2） Transposition-2 —
${\mathcal {B}}\Rightarrow {\mathcal {A}}\vdash \neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$

證明（使用T1）
（1） $\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$ （DN）（2） ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （Hyp）（3） $\neg \neg {\mathcal {B}}\Rightarrow {\mathcal {A}}$ （D with 1, 2）（4） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （DN）（5） $\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （D1 with 3,4）（6） $(\neg \neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （T1, D）（7） $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （MP with 5, 6）

注意到（T2）的證明引用了（T1）+（DN），但之前已經證明了（A1）+（A2）+（A3）可以推出（T1）；還有（A1）+（A2）+（T1）也可以推出（DN），所以註明使用（T1）即可。

以上二定理說明 ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ 推理上等價於 $\neg {\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ ，引用這兩個定理中任一都以（T）表示。

至此，已經可以證明（A1）+（A2）+（T1）可以推出（A3）：

（T1）可推出（A3）的證明
由MP律顯然有 $\neg {\mathcal {B}},\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {B}}$ （1） $\neg {\mathcal {B}}\Rightarrow [\,(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}\,]$ （對上面的定理使用兩次演繹元定理）（2） $\neg {\mathcal {B}}\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$ （D1 with 1, T2）（3） $(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {B}})\Rightarrow [\,\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\,]$ （MP with A2, 2）（4） $\neg {\mathcal {B}}\Rightarrow \neg (\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})$ （MP with I, 3）（5） $(\neg {\mathcal {B}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}$ （MP with T1, 4）（6） $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {C}})$ （Hyp）（7） $\neg {\mathcal {B}}\Rightarrow {\mathcal {C}}$ （Hyp）（8） $\neg {\mathcal {C}}\Rightarrow \neg \neg {\mathcal {B}}$ （MP with T2, 7）（9） $\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {B}}$ （D1 with 6, 8）（10） $\neg {\mathcal {B}}\Rightarrow {\mathcal {B}}$ （D1 with DN, 9）（11） ${\mathcal {B}}$ （MP with 5, 10）

所以綜合以上所述，在有（A1）+（A2）的前提下，公理（T1）等價於公理（A3）。

由（T）可以得到類似於公理（A3）的定理

（A3'） —
${\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}$

證明
（1） $(\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}]$ （A3）（2） $(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}})$ （T, D）（3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp）（4） $\neg {\mathcal {B}}\Rightarrow \neg \neg {\mathcal {A}}$ （MP with 2, 3）（5） $(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow {\mathcal {B}}$ （MP with 1, 4）（6） $({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （T, D）（7） ${\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp）（8） $\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 6, 7）（9） ${\mathcal {B}}$ （MP with 5, 8）

實質條件

以下的定理重現了實質條件的直觀理解。

（M0）material condition —
$\neg {\mathcal {A}},{\mathcal {A}}\vdash {\mathcal {B}}$

（也就是 $\neg {\mathcal {A}}\vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}$ ）

證明
（1） $\neg {\mathcal {A}}$ （Hyp）（2） ${\mathcal {A}}$ （Hyp）（3） $(\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow [(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}]$ （A3）（4） $\neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （A1）（5） $\neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 4, 1）（6） ${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})$ （A1）（7） $\neg {\mathcal {B}}\Rightarrow {\mathcal {A}}$ （MP with 6, 2）（8） $(\neg {\mathcal {B}}\Rightarrow {\mathcal {A}})\Rightarrow {\mathcal {B}}$ （MP with 3,5）（9） ${\mathcal {B}}$ （MP with 8,7）

（M1）material condition —
${\mathcal {A}},\neg {\mathcal {B}}\vdash \neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$

證明
首先注意到 ${\mathcal {A}},{\mathcal {A}}\Rightarrow {\mathcal {B}}\vdash {\mathcal {B}}$ （MP）（1） ${\mathcal {A}}\Rightarrow [({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]$ （0, D）（2） $[({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}]\Rightarrow \{\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\}$ （T）（3） ${\mathcal {A}}$ （Hyp）（4） $({\mathcal {A}}\Rightarrow {\mathcal {B}})\Rightarrow {\mathcal {B}}$ （MP with 1, 3）（5） $\neg {\mathcal {B}}\Rightarrow [\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]$ （MP with 2, 4）（6） $\neg {\mathcal {B}}$ （Hyp）（7） $\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （MP 5, 6）

（M2）material condition —
$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash \neg {\mathcal {B}}$

證明
（1） ${\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （A1）（2） $[{\mathcal {B}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})\}$ （T）（3） $[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg {\mathcal {B}})$ （MP with 1, 2）（4） $\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp）（5） $\neg {\mathcal {B}}$ （MP with 3, 4）

（M3）material condition —
$\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})\vdash {\mathcal {A}}$

證明
（1） $\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （M0, D）（2） $[\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})\}$ （T）（3） $[\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})]\Rightarrow (\neg \neg {\mathcal {A}})$ （MP with 1, 2）（4） $\neg ({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp）（5） $\neg \neg {\mathcal {A}}$ （MP with 3,4）（6） ${\mathcal {A}}$ （MP with 5, DN）

反證法

（C1）Proof by Contradiction —
${\mathcal {A}}\Rightarrow \neg {\mathcal {B}},{\mathcal {B}}\vdash \neg {\mathcal {A}}$

證明
（1） $({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})\Rightarrow (\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}})$ （T, D）（2） ${\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （Hyp）（3） $\neg \neg {\mathcal {B}}\Rightarrow \neg {\mathcal {A}}$ （MP with 1, 2）（4） ${\mathcal {B}}$ （Hyp）（5） $\neg \neg {\mathcal {B}}$ （MP with DN, 4）（6） $\neg {\mathcal {A}}$ （MP with 3, 5）

（C2）Proof by Contradiction —
$\neg {\mathcal {A}}\Rightarrow {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}$

邏輯與和邏輯或

且與或的交換性

以下為邏輯與的交換性

元定理 —
$\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow ({\mathcal {B}}\wedge {\mathcal {A}})$

證明
（1） $({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （C1, D）（2） $[({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})\Rightarrow ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow \{[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]\}$ （T, D）（3） $[\neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})]\Rightarrow [\neg ({\mathcal {B}}\Rightarrow \neg {\mathcal {A}})]$ （MP with 1,2）

類似的，（C2）正是邏輯或的交換性：

元定理 —
${\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {B}}\vee {\mathcal {A}}$ （C2, D）

且與或的直觀意義

＂且＂的直觀意義是實質條件元定理的直接結果

（AND）Intuitive meaning of And —
${\mathcal {A}},{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}$ （M1）

${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}$ （M3）

${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}$ （M2）

從（AND）和 $\Leftrightarrow$ 的符號定義可知， $\vdash {\mathcal {B}}\Leftrightarrow {\mathcal {C}}$ 的證明可以拆成兩部分；習慣上會以「（ $\Rightarrow$ ）」標示 $\vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}$ 部分的證明，而「（ $\Leftarrow$ ）」標示 $\vdash {\mathcal {C}}\Rightarrow {\mathcal {B}}$ 部分的證明。

類似的，＂或＂的直觀意義是（M0）跟（D）的直截結果

（OR）Intuitive meaning of OR —
${\mathcal {A}}\vdash {\mathcal {A}}\vee {\mathcal {B}}$ （M0, DN）

${\mathcal {B}}\vdash {\mathcal {A}}\vee {\mathcal {B}}$ （A1, D）

${\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {A}}\vdash {\mathcal {B}}$ （D）

${\mathcal {A}}\vee {\mathcal {B}},\neg {\mathcal {B}}\vdash {\mathcal {A}}$ （交換性, D）

以下的定理則是（A3'）的直截結果

（DisJ）Disjunction —
${\mathcal {A}}\Rightarrow {\mathcal {C}},{\mathcal {B}}\Rightarrow {\mathcal {C}},{\mathcal {A}}\vee {\mathcal {B}}\vdash {\mathcal {C}}$

證明
（1） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （Hyp）（2） ${\mathcal {B}}\Rightarrow {\mathcal {C}}$ （Hyp）（3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 1, 2）（4） ${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （Hyp）（5） ${\mathcal {C}}$ （A3' with 3, 4）

且與或的結合律

對於＂且＂，展開符號定義後，可以從直觀意義輕鬆地得到

（ASO-AND）Associativity of AND —
$\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\wedge {\mathcal {C}}$

＂或＂也有類似的性質

（ASO-OR）Associativity of OR —
$\vdash {\mathcal {A}}\vee ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\vee {\mathcal {C}}$

且與或的分配律

＂且＂和＂或＂之間還有分配律

（DIS-1）Distribution —
$\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})$

證明
（ $\Rightarrow$ ）（1） ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$ （Hyp）（2） ${\mathcal {A}}$ （MP with 1, AND）（3） $\neg {\mathcal {B}}\Rightarrow {\mathcal {C}}$ （MP with 1, AND）（4） $\neg \neg ({\mathcal {A}}\Rightarrow \neg {\mathcal {B}})$ （Hyp）（5） ${\mathcal {A}}\Rightarrow \neg {\mathcal {B}}$ （MP with 4, DN）（6） ${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 3, 5）（7） ${\mathcal {C}}$ （MP with 2, 5）（8） ${\mathcal {A}}\wedge {\mathcal {C}}$ （MP twice with 2, 7, AND）也就是 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg ({\mathcal {A}}\wedge {\mathcal {B}})\vdash {\mathcal {A}}\wedge {\mathcal {C}}$ 再套用（D）就會得到 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})$ （ $\Leftarrow$ ）（1） $\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}\wedge {\mathcal {C}}$ （Hyp）（2） $\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {A}}$ （D1 with 1, AND）（3） $\neg ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}$ （D1 with 1, AND）（4） $\neg {\mathcal {A}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})$ （MP with 2, C2）（5） $\neg {\mathcal {C}}\Rightarrow ({\mathcal {A}}\wedge {\mathcal {B}})$ （MP with 3, C2）（6） $\neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （D1 with 4, AND）（7） $\neg {\mathcal {C}}\Rightarrow {\mathcal {B}}$ （D1 with 4, AND）（8） ${\mathcal {A}}$ （A3' with 6, I）（9） ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$ （MP twice with 7, 8, AND）也就是 $({\mathcal {A}}\wedge {\mathcal {B}})\vee ({\mathcal {A}}\wedge {\mathcal {C}})\vdash {\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})$

（DIS-2）Distribution —
$\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$

證明
（ $\Rightarrow$ ）（1） $\neg {\mathcal {A}}\Rightarrow ({\mathcal {B}}\wedge {\mathcal {C}})$ （Hyp）（2） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （D1 with 1, AND）（3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （D1 with 1, AND）（4） $({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$ （MP twice with 2, 3,AND）也就是 ${\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})\vdash ({\mathcal {A}}\vee {\mathcal {B}})\wedge ({\mathcal {A}}\vee {\mathcal {C}})$ （ $\Leftarrow$ ）（1） $(\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})\wedge (\neg {\mathcal {A}}\Rightarrow {\mathcal {C}})$ （Hyp）（2） $\neg {\mathcal {A}}\Rightarrow {\mathcal {B}}$ （MP with 1, AND）（3） $\neg {\mathcal {A}}\Rightarrow {\mathcal {C}}$ （MP with 1, AND）（4） $\neg {\mathcal {A}}$ （Hyp）（5） ${\mathcal {B}}$ （MP with 2,4）（6） ${\mathcal {C}}$ （MP with 3,4）（7） ${\mathcal {B}}\wedge {\mathcal {C}}$ （MP twice with 5, 6, AND）也就是 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}}),\,\neg {\mathcal {A}}\vdash {\mathcal {B}}\wedge {\mathcal {C}}$ 再使用一次推論元定理會得到 ${\mathcal {A}}\wedge ({\mathcal {B}}\vee {\mathcal {C}})\vdash {\mathcal {A}}\vee ({\mathcal {B}}\wedge {\mathcal {C}})$

德摩根定律

以下的元定理的名字來自於英國邏輯學家奧古斯塔斯·德摩根。

De Morgan I —
$\vdash [\neg ({\mathcal {A}}\wedge {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\vee (\neg {\mathcal {B}})]$

證明
（ $\Rightarrow$ ）（1） $\neg \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]$ （Hyp）（2） ${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （MP with 1, DN）（3） $\neg \neg {\mathcal {A}}\Rightarrow {\mathcal {A}}$ （DN）（4） $\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （D1 with 2, 3）（ $\Leftarrow$ ）（1） $\neg \neg {\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （Hyp）（2） ${\mathcal {A}}\Rightarrow \neg \neg {\mathcal {A}}$ （DN）（3） ${\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})$ （D1 with 1, 2）（4） $\neg \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {B}})]$ （MP with DN, 3）

De Morgan II —
$\vdash [\neg ({\mathcal {A}}\vee {\mathcal {B}})]\Leftrightarrow [(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})]$

證明
（ $\Rightarrow$ ）（1） $\neg (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （Hyp）（2） $\neg {\mathcal {A}}$ （MP with M2, 1）（3） $\neg {\mathcal {B}}$ （MP with M3, 1）（4） $(\neg {\mathcal {A}})\wedge (\neg {\mathcal {B}})$ （AND with 2, 3）（ $\Leftarrow$ ）（1） $\neg {\mathcal {A}}$ （Hyp）（2） $\neg {\mathcal {B}}$ （Hyp）（3） $\neg (\neg {\mathcal {A}}\Rightarrow {\mathcal {B}})$ （M1）

普遍化元定理

公理模式（A7）可以稍加延伸成以下的元定理

定理的普遍化 —

對任意變數 $x$ ，若 $\vdash {\mathcal {B}}$ 則有 $\vdash (\forall x){\mathcal {B}}$ 。

證明
假設 ${\mathcal {C}}_{1},{\mathcal {C}}_{2},....,{\mathcal {C}}_{n}$ 就是 ${\mathcal {B}}$ 的證明，那 ${\mathcal {C}}_{1}$ 一定是公理，根據（A7）可以得到 $\vdash (\forall x){\mathcal {C}}_{1}$ 若對 $i<k$ 都有 $\vdash (\forall x){\mathcal {C}}_{i}$ ，如果 ${\mathcal {C}}_{k}$ 是公理的話顯然 $\vdash (\forall x){\mathcal {C}}_{k}$ 。若有 $l,m<k$ 使得 ${\mathcal {C}}_{m}:{\mathcal {C}}_{l}\Rightarrow {\mathcal {C}}_{k}$ 那根據歸納法的假設跟（A6）有 $\vdash (\forall x){\mathcal {C}}_{l}\Rightarrow (\forall x){\mathcal {C}}_{k}$ 上式配上 $\vdash (\forall x){\mathcal {C}}_{l}$ 就可以得到 $\vdash (\forall x){\mathcal {C}}_{k}$ 以此歸納到 ${\mathcal {C}}_{n}$ 也就是 ${\mathcal {B}}$ ，故本元定理得證。 $\Box$

更進一步，有以下元定裡

（GEN） —
在 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}$ 裡變數 $x$ 都完全被約束，若

{\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash {\mathcal {B}}

則有

{\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{n}\vdash (\forall x){\mathcal {B}}

證明
以下對前提條件的數量 $n$ 做歸納。若 $n=1$ ，根據前提有 ${\mathcal {A}}_{1}\vdash {\mathcal {B}}$ 以（D）將 ${\mathcal {A}}_{1}$ 往前搬，再套用定理的普遍化，會得到 $\vdash (\forall x)({\mathcal {A}}_{1}\Rightarrow {\mathcal {B}})$ 再根據（A5）和MP律，就可以得到 $\vdash {\mathcal {A}}_{1}\Rightarrow (\forall x){\mathcal {B}}$ 也就是本元定理要求的結果。現在假設 $n<k$ 的情況下元定理會成立。元定理的前提條件根據（D）可以寫為 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash {\mathcal {A}}_{k}\Rightarrow {\mathcal {B}}$ 則根據歸納法的假設 ${\mathcal {A}}_{1},{\mathcal {A}}_{2},....,{\mathcal {A}}_{k-1}\vdash (\forall x)({\mathcal {A}}_{k}\Rightarrow {\mathcal {B}})$ 上式配上（A5），本元定理在 $n=k$ 的情況就可以得到證明，故本元定理得證。 $\Box$

（GEN）可以稍加修飾，以套用在含有存在量詞的公式上

（GENe） —

若變數 $x$ 在 $\Gamma$ 的公式和 ${\mathcal {C}}$ 裡都完全被約束則

（1）若 $\Gamma \vdash {\mathcal {A}}\Rightarrow {\mathcal {B}}$ 則 $\Gamma \vdash (\exists x){\mathcal {A}}\Rightarrow (\exists x){\mathcal {B}}$

（2）若 $\Gamma \vdash {\mathcal {B}}\Rightarrow {\mathcal {C}}$ 則 $\Gamma \vdash (\exists x){\mathcal {B}}\Rightarrow {\mathcal {C}}$

等價代換

以下的定理，說明兩條「等價」的公式可以互相代換

（Equv）Equivalence of WF —
$\Gamma$ 代表一群公式，若公式 ${\mathcal {A}}$ 和 ${\mathcal {B}}$ 滿足：

\Gamma \vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}

則對變數 $x$ 和任意公式 ${\mathcal {C}}$ ：

$\Gamma \vdash (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})$
$\Gamma \vdash ({\mathcal {C}}\Rightarrow {\mathcal {A}})\Leftrightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})$
$\Gamma \vdash ({\mathcal {A}}\Rightarrow {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$
變數 $x$ 於 $\Gamma$ 完全被約束，則

\Gamma \vdash (\forall x){\mathcal {A}}\Leftrightarrow (\forall x){\mathcal {B}}

證明
以下的證明都會用到這三條公式： (a) ${\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ （from $\Gamma$ ） (b) ${\mathcal {A}}\Rightarrow {\mathcal {B}}$ （MP with AND, a） (c) ${\mathcal {B}}\Rightarrow {\mathcal {A}}$ （MP with AND, a） 1. (1) $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})$ （MP with T, b） (2) $(\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})$ （MP with T, c） (3) $(\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})$ （AND with 3, 5） 2. ( $\Rightarrow$ ) (1) ${\mathcal {C}}\Rightarrow {\mathcal {A}}$ （Hyp） (2) ${\mathcal {C}}\Rightarrow {\mathcal {B}}$ （D1 with 1, b） ( $\Leftarrow$ ) (1) ${\mathcal {C}}\Rightarrow {\mathcal {B}}$ （Hyp） (2) ${\mathcal {C}}\Rightarrow {\mathcal {A}}$ （D1 with 1, c） 3. ( $\Rightarrow$ ) (1) ${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （Hyp） (2) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})$ （MP with T, 1） (3) $(\neg {\mathcal {A}})\Rightarrow (\neg {\mathcal {B}})$ （MP with T, c） (4) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})$ （D1 with 2, 3） (5) ${\mathcal {B}}\Rightarrow {\mathcal {C}}$ （MP with T, 4） ( $\Leftarrow$ ) (1) ${\mathcal {B}}\Rightarrow {\mathcal {C}}$ （Hyp） (2) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {B}})$ （MP with T, 1） (3) $(\neg {\mathcal {B}})\Rightarrow (\neg {\mathcal {A}})$ （MP with T, b） (4) $(\neg {\mathcal {C}})\Rightarrow (\neg {\mathcal {A}})$ （D1 with 2, 3） (5) ${\mathcal {A}}\Rightarrow {\mathcal {C}}$ （MP with T, 4） 4. ( $\Rightarrow$ ) (1) $(\forall x)({\mathcal {A}}\Rightarrow {\mathcal {B}})$ （GEN with $x$ , a） (2) $(\forall x){\mathcal {A}}\Rightarrow (\forall x){\mathcal {B}}$ （MP with A6 , 1） ( $\Leftarrow$ ) (1) $(\forall x)({\mathcal {B}}\Rightarrow {\mathcal {A}})$ （GEN with $x$ , c） (2) $(\forall x){\mathcal {B}}\Rightarrow (\forall x){\mathcal {A}}$ （MP with A6 , 1）

這些定理通常是混合使用，以達到「等價代換」的結果，例如，考慮到「邏輯與」是以下的符號定義：

({\mathcal {A}}\wedge {\mathcal {C}}):=\neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]

那如果假設 $\vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ ，就有：

$\vdash [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]$
$\vdash \neg [{\mathcal {A}}\Rightarrow (\neg {\mathcal {C}})]\Leftrightarrow \{\neg [{\mathcal {B}}\Rightarrow (\neg {\mathcal {C}})]\}$

換句話說，從「 $\vdash {\mathcal {A}}\Leftrightarrow {\mathcal {B}}$ 」可以得到「 $\vdash ({\mathcal {A}}\wedge {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\wedge {\mathcal {C}})$ 」，直觀上相當於，把 ${\mathcal {A}}$ 都代換成 ${\mathcal {B}}$ 則兩式等價。日後像這樣遞迴地套用上述定理來得到「代換則某兩式等價」，都簡單地以「引用（Equv）」來表示這段實際的推演過程。

量詞的可交換性

由普遍化，很容易證明以下關於＂交換性＂的定理

元定理 —
（1） $(\forall x)(\forall y){\mathcal {A}}\vdash (\forall y)(\forall x){\mathcal {A}}$

（2） $(\exists x)(\exists y){\mathcal {A}}\vdash (\exists y)(\exists x){\mathcal {A}}$

（3） $(\exists x)(\forall y){\mathcal {A}}\vdash (\forall y)(\exists x){\mathcal {A}}$

注意最後（3）一般來說是不能反向的，只要想到＂對每個 $a$ ，都有一個數（也就是 $-a$ ），使 $a+(-a)=0$ ＂，但是任取一個 $a$ 的數 $(-a)$ 和任意的數 $b$ ， $b+(-a)$ 並不一定會為零。

量詞的簡寫

數學中常常有＂對所有 $\epsilon >0$ 有...＂，或是＂存在 $\delta >0$ 使的...＂。而兩句話比較清晰，接近一階邏輯語言的說法是＂對所有 $\epsilon$ ，只要 $\epsilon >0$ 則...＂與＂存在 $\delta$ ， $\delta >0$ 且...＂。「大於」直觀上是一個二元关系，也就是說，在公理化集合論裡對應於一條 $\epsilon$ （或 $\delta$ ）在裡面完全自由的合式公式。據此，可做以下的符號定義

符號定義 —
如果變數 $x$ 和 $y$ 都於合式公式 ${\mathcal {A}}(x,\,y)$ 裡完全自由，那

$[\,\forall {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\forall x)[\,{\mathcal {A}}(x,\,y)\Rightarrow {\mathcal {B}}\,]$

$[\,\exists {\mathcal {A}}(x,\,y)\,]{\mathcal {B}}:=(\exists x)[\,{\mathcal {A}}(x,\,y)\wedge {\mathcal {B}}\,]$

但直觀上也會說＂對所有 $n>0$ 和 $m>0$ 有...＂，這樣連續，帶有條件的全稱量詞也是有＂交換性＂的。為了討論這個問題，首先需要一些前置的定理

（abb） —
$\vdash [{\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})]\Leftrightarrow [({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}]$

證明
（ $\Rightarrow$ ） ${\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})\vdash ({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}$ 注意到（AND） ${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {A}}$ （AND） ${\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {B}}$ 所以 ${\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}}),\,{\mathcal {A}}\wedge {\mathcal {B}}\vdash {\mathcal {C}}$ 再套上演繹元定理就可以得證。 $\Box$ （ $\Leftarrow$ ） $({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}}\vdash {\mathcal {A}}\Rightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$ 注意到（AND） ${\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {A}}\wedge {\mathcal {B}}$ 所以 $({\mathcal {A}}\wedge {\mathcal {B}})\Rightarrow {\mathcal {C}},\,{\mathcal {A}},\,{\mathcal {B}}\vdash {\mathcal {C}}$ 再套上演繹元定理就可以得證。 $\Box$

這樣就可以證明以下定理

元定理 —
如果變數 $x$ 和 $y$ 都於合式公式 ${\mathcal {A}}(x,\,y)$ 和 ${\mathcal {B}}(x,\,y)$ 裡完全自由，若項 $T$ 裡沒有 $y$ 那

$\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow \forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {C}}\}$

證明
（ $\Rightarrow$ ） $[\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\vdash \forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}$ （1） $(\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （Hyp）（2） ${\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with 1, A4）（3） ${\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （D1 with 2, A4）（4） $[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {C}}$ （MP with abb, 3）（5） $\forall x\forall y\{[{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)]\Rightarrow {\mathcal {B}}\}$ （GEN with 4 twice）（ $\Leftarrow$ ） $\forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}$ （1） $\forall x\forall y\{[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}\}$ （Hyp）（2） $[\,{\mathcal {A}}(x,\,T)\wedge {\mathcal {B}}(y,\,S)\,]\Rightarrow {\mathcal {B}}$ （MP with 2, A4 twice）（3） ${\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with abb, 2）（4） $(\forall y)\{\,{\mathcal {A}}(x,\,T)\Rightarrow [\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （GEN with 3）（5） ${\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]$ （MP with A5, 4）（6） $(\forall x)\{\,{\mathcal {A}}(x,\,T)\Rightarrow (\forall y)[\,{\mathcal {B}}(y,\,S)\Rightarrow {\mathcal {C}}\,]\,\}$ （GEN with 5）

如果再加上＂項 $S$ 裡沒有 $x$ ＂那就是＂對所有 $n>0$ 和 $m>0$ 有...＂，也就是以上所討論的情況了。以這個定理配上全稱量詞本身的交換性定理，那這句話就可以等價的說成＂對所有 $m$ 和 $n$ 若 $n>0$ 且 $m>0$ 則...＂，所以根據＂且＂的可交換性，可以進一步的說成＂對所有 $m>0$ 和 $n>0$ 有...＂，所以連續帶有條件的全稱量詞是＂可交換的＂。也就是說

元定理 —
如果變數 $x$ 和 $y$ 都於合式公式 ${\mathcal {A}}(x,\,y)$ 和 ${\mathcal {B}}(x,\,y)$ 裡完全自由，若項 $T$ 裡沒有 $y$ ，且項 $S$ 裡沒有 $x$ 則

$\vdash [\,\forall {\mathcal {A}}(x,\,T)\,][\,\forall {\mathcal {B}}(y,\,S)\,]{\mathcal {C}}\Leftrightarrow [\,\forall {\mathcal {B}}(y,\,S)\,][\,\forall {\mathcal {A}}(x,\,T)\,]{\mathcal {C}}$

但對於帶條件的存在量詞，首先可以得到以下非等價的定理。

元定理 —
$(\exists x)(\exists y)({\mathcal {A}}\wedge {\mathcal {B}}\wedge {\mathcal {C}})\vdash (\exists x)[\,{\mathcal {A}}\wedge (\exists y)({\mathcal {B}}\wedge {\mathcal {C}})\,]$

這是因為一般來說， $(\exists y){\mathcal {D}}$ 不總是能推出 ${\mathcal {D}}$ 。雖說如此，只要對公式做出一些限制，就會有以下交換的直觀定理：

（Ce）－Commutativity of existential quantification —
若變數 $x$ 於公式 ${\mathcal {Q}}$ 完全被約束，且 ${\mathcal {R}}$ 是另外一條公式，則：

\vdash (\exists x)({\mathcal {R}}\wedge {\mathcal {\mathcal {Q}}})\Leftrightarrow [(\exists x)({\mathcal {R}})\wedge {\mathcal {Q}})]

證明
( $\Rightarrow$ ) (1) ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})$ (Hyp) (2) ${\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})$ (D1 with 1 and A4) 換句話說 ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash {\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})$ 這樣使用(GEN)有 ${\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})\vdash (\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]$ 這樣對上式使用(De Morgan)和(T)就有 $\vdash (\exists x)({\mathcal {R}}\wedge {\mathcal {\mathcal {Q}}})\Rightarrow [(\exists x)({\mathcal {R}})\wedge {\mathcal {Q}})]$ ( $\Leftarrow$ ) (1) $(\forall x)[{\mathcal {Q}}\Rightarrow (\neg {\mathcal {R}})]\Rightarrow [{\mathcal {Q}}\Rightarrow (\forall x)(\neg {\mathcal {R}})]$ (A5) (2) $(\forall x)[(\neg {\mathcal {Q}})\vee (\neg {\mathcal {R}})]\Rightarrow [(\neg {\mathcal {Q}})\vee (\forall x)(\neg {\mathcal {R}})]$ ( $\vee$ 的定義) (3) $(\forall x)[\neg ({\mathcal {Q}}\wedge {\mathcal {R}})]\Rightarrow \{\neg [({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\}$ (MP with 2, De Morgan) (4) $[({\mathcal {Q}})\vee (\exists x)({\mathcal {R}})]\Rightarrow (\exists x)({\mathcal {Q}}\wedge {\mathcal {R}})$ (MP with 3, T)

也就是直觀上，「存在x使得 x>0 且 y>0」與｢y>0 且存在x使得 x>0」是一樣的意思。

等式定理

一般來說，等式 $(x=y)$ 會被視為某個合式公式 ${\mathcal {E}}(x,\,y)$ 的簡寫。若使用元定理的形式刻劃等式的性質，會作如下的定義

元定義 —
說一階邏輯理論 ${\mathcal {L}}$ 帶相等符號 ${\mathcal {E}}(x,\,y)$ 意為（ $x_{1},\,\cdots ,\,x_{n}$ 、 $x$ 和 $y$ 都是 ${\mathcal {L}}$ 的任意變數）

除了變數 $x$ 和 $y$ 於 ${\mathcal {E}}(x,\,y)$ 是完全自由外其他變數都完全被約束
（E1） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,x)$ 。
（E2'） ${\mathcal {B}}(x,\,x)$ 為 ${\mathcal {L}}$ 內不含函數符號與常數符號的原子公式 ， $x$ 若以 ${\mathcal {B}}(x,\,y)$ 表示 ${\mathcal {B}}(x,\,x)$ 內某一個 $x$ 被取代成 $y$ 而成的新公式，則有

\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]

（E2＂）若以 $f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})$ 代表項 $f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})$ 裡的 $x_{k}$ 被取代成 $y$ 而成的新項，則有

\vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]

（E3） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(y,\,x)$ 。

並在這種狀況下，規定 $(x=y)$ 為 ${\mathcal {E}}(x,\,y)$ 的簡寫。

上面的定義符合函數符號直觀上的＂唯一對應＂。為了證明常數符號的＂唯一性＂，需要以下元定理

元定理 —
說一階邏輯理論 ${\mathcal {L}}$ 帶相等符號 ${\mathcal {E}}(x,\,y)$ ，等同於要求：

${\mathcal {E}}(x,\,y)$ 除了變數 $x$ 和 $y$ 於 ${\mathcal {E}}(x,\,y)$ 是完全自由外其他變數都完全被約束。
符合（E1）。
（E2）對於任意變數 $x$ 和 $y$ ，若在公式 ${\mathcal {A}}$ 中自由的 $y$ 都不在 $\forall x$ 的範圍內。若以 ${\mathcal {A}}_{y}$ 代表 ${\mathcal {A}}$ 某些自由的 $x$ 被取代成 $y$ 而成的新公式，則

\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow ({\mathcal {A}}\Rightarrow {\mathcal {A}}_{y})

證明
（ $\Rightarrow$ ）從（E1）+（E2'）+（E2＂）+（E3）推出（E2）的過程分成幾個階段推廣（E2'）（1）含有常數符號的原子公式取 $c_{j}$ 為任意常數符號。目標是證明：對一段含常數符號 $c_{j}$ 但不含任何函數符號的原子公式 ${\mathcal {B}}(x,\,x,\,c_{j})$ ，若 ${\mathcal {B}}(x,\,y,\,c_{j})$ 表 ${\mathcal {B}}(x,\,x,\,c_{j})$ 裡某一個 $x$ 被取代為 $y$ 的新公式，則 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]$ （a）（a）證明過程如下：取一個不曾在 ${\mathcal {B}}(x,\,y,\,c_{j})$ 出現的變數 $z$ 。若以 ${\mathcal {B}}(x,\,x,\,z)$ 表示 ${\mathcal {B}}(x,\,x,\,c_{j})$ 內的 $c_{j}$ 都被取代成 $z$ 的新公式，將之帶入（E2'）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]$ 對上式，以變數 $z$ 取（GEN）有 $\vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}$ （b）但從（A4）有 $\vdash _{\mathcal {L}}\forall z\{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,z)\Rightarrow {\mathcal {B}}(x,\,y,\,z)]\}\Rightarrow \{{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x,\,c_{j})\Rightarrow {\mathcal {B}}(x,\,y,\,c_{j})]\}$ 這樣上式就可以與（b）式取MP，就會有（a）。（2）含有任意項的原子公式對一列項 $T_{1},\,\cdots ,\,T_{m}$ ，若以 $S$ 代表項 $T_{k}$ 裡的一個 $x$ 被取代成 $y$ 而成的新項，那這樣可以用 $A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})$ 代表 $A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})$ 的 $T_{k}$ 被取代成 $S$ 所構成的新公式。那現在的目標是證明 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(T_{1},\,\cdots ,\,T_{k},\,\cdots ,\,T_{m})\Rightarrow A_{j}^{m}(T_{1},\,\cdots ,\,S,\,\cdots ,\,T_{m})]$ （c）但根據（A4）和（GEN），只需要證明 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]$ （c'）就足夠了。更進一步的，由下面兩定理可以推出（c'） $\vdash _{\mathcal {L}}{\mathcal {E}}(z,\,z^{\prime })\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z,\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,z^{\prime },\,x_{k+1},\,\cdots ,\,x_{m})]$ （d） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)$ （e）也就是對（c）以變數 $z$ 和 $z^{\prime }$ 連續兩次使用（GEN），然後連續兩次與（A4）以MP律配合會得到 $\vdash _{\mathcal {L}}{\mathcal {E}}(T_{k},\,S)\Rightarrow [A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,T_{k},\,x_{k+1},\,\cdots ,\,x_{m})\Rightarrow A_{j}^{m}(x_{1},\,\cdots ,\,x_{k-1},\,S,\,x_{k+1},\,\cdots ,\,x_{m})]$ 然後將上式與（e）帶入（D1）就有（c'）。但事實上（d）就是（E2'）的特殊狀況，所以接下來只需要從（E2＂）證明（e），為此根據項的遞迴定義，以對項 $T_{k}$ 裡有的函數符號數量做歸納：函數符號數量為零的時候，（e）有兩種狀況（其中 $c_{j}$ 為任意常數符號） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(x,\,y)$ （e0） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(c_{j},\,c_{j})$ （e0'）（e0）就只是（I）故顯然成立；另一方面，對（E1）使用（GEN）然後與（A4）配合就會有 $\vdash _{\mathcal {L}}{\mathcal {E}}(c_{j},\,c_{j})$ 故與（A1）配合就會有（e0'），至此函數符號數量為零情況的（e）已被證明。若 $T_{k}$ 內函數符號數量為 $l$ 個，事實上會有一列函數符號數量小於 $l$ 的項 $S_{1},\,\cdots ,\,S_{n}$ ，而有 $T_{k}:f_{i}^{n}(S_{1},\,\cdots ,\,S_{n})$ 若以 ${S_{r}}^{\prime }$ 代表 $S_{r}$ 中的某個 $x$ 被取代成 $y$ 而成的新項，那這就是 $T_{k}$ 取代成新項 $S$ 的詳細過程，那歸納法的前提就是 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })$ 那對（E2＂）使用 $n$ 次（GEN），然後同樣與（A4）以MP律配合 $n$ 次有 $\vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}[f_{i}^{n}(S_{1},\,\cdots ,\,S_{r},\,\cdots ,\,S_{n}),\,f_{i}^{n}(S_{1},\,\cdots ,\,{S_{r}}^{\prime },\,\cdots ,\,S_{n})]$ 也就是 $\vdash _{\mathcal {L}}{\mathcal {E}}(S_{r},\,{S_{r}}^{\prime })\Rightarrow {\mathcal {E}}(T_{k},\,S)$ 故將上式與歸納前提套入（D1）就會有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow {\mathcal {E}}(T_{k},\,S)$ 至此（e）已被歸納法證明。（3）任意的公式為了將（E2'）從任意原子公式推廣到任意公式，根據語法對公式的遞迴定義，要分別對公式裡的量詞和邏輯連接詞的數量做歸納。假設 ${\mathcal {B}}(x,\,x)$ 為不含邏輯連接詞的任意公式： ${\mathcal {B}}(x,\,x)$ 沒有量詞的情況就只是（c）而已，故成立。若假設對於量詞數量為 $l$ 的 ${\mathcal {B}}(x,\,x)$ 有（ ${\mathcal {B}}(x,\,y)$ 代表 ${\mathcal {B}}(x,\,x)$ 內某個自由的 $x$ 被取代成 $y$ 所成的新公式） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]$ 首先注意到新增量詞的時候，不可以取 $\forall x$ 或是 $\forall y$ ，否則上面的自由取代就會完全被破壞。故取個不是 $x$ 也不是 $y$ 的任意變數 $z$ ，對上式使用（GEN），然後與（A6）、（A5）配合使用MP律有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\forall z{\mathcal {B}}(x,\,x)\Rightarrow \forall z{\mathcal {B}}(x,\,y)]$ 上式也就是量詞數量為 $l+1$ 的狀況，而把（E2'）推廣到了不含邏輯連接詞的任意公式上。接下來對不含「 $\Rightarrow$ 」的任意公式裡的「 $\neg$ 」的數量做歸納：「 $\neg$ 」的數量為零的情況剛剛已經證明，不再贅述。假設「 $\neg$ 」的數量為 $l$ ，沒有「 $\Rightarrow$ 」的公式下（E2'）都對，那對「 $\neg$ 」的數量為 $l$ 的 ${\mathcal {B}}(x,\,x)$ 有（特別注意到推廣的（E2'）也可以將 ${\mathcal {B}}(x,\,y)$ 裡唯一的 $y$ 取代成 $x$ ） $\vdash _{\mathcal {L}}{\mathcal {E}}(y,\,x)\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]$ （f）那根據（T）有 $\vdash _{\mathcal {L}}[{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x)]\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]$ （g）這樣對（f）和（g）套用（D1），結果再和（E3）套用（D1）一次就有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [\neg {\mathcal {B}}(x,\,x)\Rightarrow \neg {\mathcal {B}}(x,\,y)]$ （f）上式也就「 $\neg$ 」的數量為 $l+1$ 的情況，故把（E2'）推廣到了僅不含「 $\Rightarrow$ 」的任意公式上。為了要推廣到任意的公式上，我要要對「 $\Rightarrow$ 」的數量做歸納：「 $\Rightarrow$ 」的數量為零的情況剛剛已經證明，不再贅述。假設「 $\Rightarrow$ 」的數量小於 $l$ 的公式下（E2'）都對，那對但數量合起來為 $l$ 的 ${\mathcal {B}}(x,\,x)$ 與 ${\mathcal {C}}(x,\,x)$ 就會滿足 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {B}}(x,\,y)]$ （） $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]$ （）考慮到（D1）有 ${\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x),\,{\mathcal {C}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)$ ${\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {B}}(x,\,x),\,{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)\,\vdash _{\mathcal {L}}{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)$ 那配上（）與（**）就有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,y)]\}$ $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow \{[{\mathcal {B}}(x,\,x)\Rightarrow {\mathcal {C}}(x,\,x)]\Rightarrow [{\mathcal {B}}(x,\,y)\Rightarrow {\mathcal {C}}(x,\,x)]\}$ 上兩式就是所有「 $\Rightarrow$ 」的數量為 $l+1$ 的情況，故把（E2'）推廣到了任意公式。最後，取代 $n+1$ 個 $x$ 的狀況，就是取代 $n$ 後再取代一次。所以可以由歸納法，從推廣後的（E2'）推出（E2）（ $\Leftarrow$ ）首先（E2'）顯然只是（E2）的特例；要得到（E2＂）只要注意到由（E2）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x_{k},\,y)\Rightarrow \{{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]\Rightarrow {\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,y,\,\cdots ,\,x_{n})]\}$ 然後對（E1）使用（GEN）再配合（A4）使用MP律有 $\vdash _{\mathcal {L}}{\mathcal {E}}[f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n}),\,f_{i}^{n}(x_{1},\,\cdots ,\,x_{k},\,\cdots ,\,x_{n})]$ 所以對上面兩式套用（D2）就有（E2＂）。至於（E3），注意到由（E2）有 $\vdash _{\mathcal {L}}{\mathcal {E}}(x,\,y)\Rightarrow [{\mathcal {E}}(x,\,x)\Rightarrow {\mathcal {E}}(y,\,x)]$ 那這樣對上式和（E1）套用（D2）就有（E3）

從上面可以得知，如果等式符號僅僅為斷言符號，那等式和它的公理一節的等式公理模式，是等價於本節的（E1）+（E2'）+（E2＂）。

由上面的元定理，對帶有等式符號的 ${\mathcal {L}}$ 可以證明以下的等式性質

元定理 —
若 $T$ 、 $S$ 與 $R$ 為 ${\mathcal {L}}$ 的任意項，則有

$\vdash _{\mathcal {L}}T=T$
$\vdash _{\mathcal {L}}(T=S)\Rightarrow (S=T)$
$\vdash _{\mathcal {L}}(S=T)\Rightarrow [(S=R)\Rightarrow (T=R)]$

證明提示：

（E1）+（GEN）+（A4）。
將 $(x=x)$ 帶入（E2）後使用（D2），然後套用兩次（GEN）+（A4）即可。
注意到從（E2）有 $\vdash _{\mathcal {L}}(x=y)\Rightarrow [(x=z)\Rightarrow (y=z)]$ ，然後套用三次（GEN）+（A4）即可。

對任意常數符號 $c$ ，上列元定理確保了

\vdash _{\mathcal {L}}(c=c)

(x=c),\,(y=c)\vdash _{\mathcal {L}}(x=y)

也就是常數符號的＂唯一性＂。

函數符號與唯一性

唯一性

數學討論中，常常唯一存在某個符合特定條件的數，像是「存在唯一的實數 $s\in \mathbb {R}$ 使的對所有的实数 $r\in \mathbb {R}$ ， $r+s=r$ 」；更精確地來說，這句話的意思是：

「存在

s\in \mathbb {R}

使的對所有的實數

r\in \mathbb {R}

，

r+s=r

」且「對所有的

s^{\prime },\,s\in \mathbb {R}

和所有

r\in \mathbb {R}

，若

r+s=r

且

r+s^{\prime }=r

則

s=s^{\prime }

」

這樣一般來說，可以對任意變數 $x$ 和合式公式 ${\mathcal {B}}(x)$ 做以下的符號定義：

符號定義 —
$\exists !x{\mathcal {B}}(x):=\exists x{\mathcal {B}}(x)\wedge (\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]$

（其中 $y$ 必須是展開以上定義時首次出現的變數； ${\mathcal {B}}(y)$ 是將 ${\mathcal {B}}(x)$ 內自由的 $x$ 都取代成 $y$ 所形成的新公式。）

注意到要能定義唯一性，一階邏輯理論一定要帶有等號。

新舊理論的等效條件

上節所提到的例子，實際上就是所謂的實數 $0$ ，但常數符號不能憑空從理論中冒出來，所以仔細來說，「定義實數 $0$ 」的過程應該是在原來的理論添加新的常數符號「 $0$ 」與以下的公理：

「對所有的實數

r\in \mathbb {R}

有

r+0=r

」

這樣的話，「 $r>0$ 」就是一條含有新常數符號的敘述，它應等價於：

存在

s\in \mathbb {R}

使「

r>s

且對所有的

x\in \mathbb {R}

，

x+s=x

」

也就是說，添加「 $0$ 」創造了一套新理論，新理論的每條新敘述會對應到舊理論的某條舊敘述，且照理來說，新的對舊的也會對，反之亦然。

更一般的來說，如果新的一階邏輯理論，是在舊的理論增添一些新符號跟新公理（並額外要求新符號與舊公理相容），那為了讓新舊理論等效，對於任意新理論的合式公式 ${\mathcal {C}}$ ，都要有某條相應的舊理論公式 ${\mathcal {C}}^{\prime }$ 滿足以下條件：

新舊理論的等價條件 —
（ $\vdash _{o}$ 代表舊理論可以推出； $\vdash _{n}$ 代表新理論可以推出。）

（1）若 ${\mathcal {C}}$ 本來就內含在舊理論裡，則 ${\mathcal {C}}^{\prime }$ 就是 ${\mathcal {C}}$ 。

（2） $\vdash _{n}{\mathcal {C}}^{\prime }\Leftrightarrow {\mathcal {C}}$

（3）若 $\vdash _{n}{\mathcal {C}}$ ，則有 $\vdash _{o}{\mathcal {C}}^{\prime }$ 。

從條件（2）事實上就可以推出「若 $\vdash _{o}{\mathcal {C}}^{\prime }$ ，則有 $\vdash _{n}{\mathcal {C}}$ 」，因為 $\vdash _{o}{\mathcal {C}}^{\prime }$ 的話，新理論只是擴張舊理論而沒改變舊理論固有的定理，所以有 $\vdash _{n}{\mathcal {C}}^{\prime }$ ，但這樣根據條件（2）跟MP律就會有 $\vdash _{n}{\mathcal {C}}$ 。所以條件（2）事實上是比「舊的對那新的也對」強的條件，但在之後的推導上（2）會比較方便。

預備定理

在以嚴謹的方式實踐以上提及的直觀動機前，需要一個預備定理

元定理 —
變數 $x$ 在和合式公式 ${\mathcal {B}}(x)$ 與 ${\mathcal {C}}(x)$ 完全自由，則有

（Aux） $\exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Leftrightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$

證明
（ $\Rightarrow$ ） $\exists !{\mathcal {B}}(x)\vdash (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\Rightarrow (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ 以下取一個不曾出現的變數 $y$ 展開唯一性的定義（1） $(\forall x)(\forall y)[\,{\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)\,]$ （Hyp）（2） ${\mathcal {B}}(y)$ （Hyp）（3） ${\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ （Hyp）（4） ${\mathcal {B}}(x)\wedge {\mathcal {B}}(y)\Rightarrow (x=y)$ （MP with A4, 1）（5） ${\mathcal {B}}(x)$ （MP with AND, 3）（6） ${\mathcal {B}}(x)\wedge {\mathcal {B}}(y)$ （MP twice with AND, 2, 5）（7） $(x=y)$ （MP with 4, 6）（8） $(x=y)\Rightarrow [\,{\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)\,]$ （E2）（9） ${\mathcal {C}}(x)\Rightarrow {\mathcal {C}}(y)$ （MP with 7, 8）（10） ${\mathcal {C}}(x)$ （MP with AND, 3）（11） ${\mathcal {C}}(y)$ （MP with 9, 10）這樣根據（AND）和 (D1) 有 $\exists x!{\mathcal {B}}(x),\,{\mathcal {B}}(y),\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,\vdash \,{\mathcal {C}}(y)$ 那這樣先使用（D）把 ${\mathcal {B}}(y)$ 移到左邊，並對變數 $x$ 使用（GENe）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)$ 那這樣再對變數 $y$ 使用（GEN）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists y[\,{\mathcal {B}}(y)\Rightarrow {\mathcal {C}}(y)\,]$ 再使用（A4）把右側的變數 $y$ 替換成 $x$ ，再對 $x$ 使用（GEN）有 $\exists x!{\mathcal {B}}(x),\,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]\,\vdash \,\exists x[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ 所以根據（D），本部分得証。（ $\Leftarrow$ ） $\exists !{\mathcal {B}}(x)\vdash (\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]\Rightarrow (\exists x)[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ （1） $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,]$ （Hyp）（2） ${\mathcal {B}}(x)$ （Hyp）（3） ${\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)$ （MP with A4, 1）（4） ${\mathcal {C}}(x)$ （MP with 2, 3）（4） ${\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ （MP twice with AND, 2, 4）也就是說 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,{\mathcal {B}}(x)\,\vdash \,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)$ 對變數 $x$ 使用（GENe）有 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ 這樣根據（AND）和 (D1) 有 $(\forall x)[\,{\mathcal {B}}(x)\Rightarrow {\mathcal {C}}(x)\,],\,\exists !x{\mathcal {B}}(x)\,\vdash \,\exists x[\,{\mathcal {B}}(x)\wedge {\mathcal {C}}(x)\,]$ 所以根據（D），本部分得証。

新理論的假設

一般來說，如果變數 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$ 在 ${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ 完全自由，且舊理論裡有：

（

U

）

\vdash _{o}\exists !x{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)

那所謂的新理論，就是添加一個函數符號 $f_{k}^{n}$ 和以下的新公理：

（

U^{\prime }

）

{\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]

如果僅僅是：

\vdash _{o}\exists !x{\mathcal {B}}(x)