一階邏輯

一階邏輯是使用於數學、哲學、語言學及電腦科學中的一種形式系統，也可以稱為：一階斷言演算、低階斷言演算、量化理論或謂詞邏輯。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。

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

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

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

簡介

基本符號

命題邏輯顧名思義，會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假的敘述簡記為 $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)\}$

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

形式理論

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

1. 語法：決定哪些符號組合是合式公式。（直觀上的「文法無誤的敘述」）
2. 推理規則：由合式公式符號組合出新合式公式的規則（直觀上的「推理」）
3. 公理：一套合式公式（直觀上的基本假設）

基本符號

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

邏輯符號

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

1. 量化符號 $\forall$ 及 $\exists$
   • 某些作者會把 $\exists$ 符號定義為 $\exists x{\mathcal {A}}:=\neg [\forall x(\neg {\mathcal {A}})]$，如此便只需要 $\forall$ 做為基礎符號。
2. 邏輯聯結詞：以下為可能的表示符號（關於波蘭表示法下的邏輯連接詞，請參見邏輯運算的波蘭記法）：
   • 否定： $\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}}),$

   如此一來只需要否定和條件做為基礎符號。

3. 標點符號：括號、逗號及其他，依作者的喜好有所不同。
   • 為了更有效的將括號做配對，通常還會採用大括號{ }跟中括號[ ]。
4. 至多跟自然數一樣多的變數，通常標記為英文字母末端的小寫字母x、y、z、…，也常會使用下標（或上標、上下標兼有）來區別不同的變數：x₀、x₁、x₂、…（特別注意c有時候會被當成常數符號而引起混淆）。
5. 等式符號：$=$
   • 有作者會因為語義上對「相等」的不同解釋，而將等式符號視為雙元斷言符號、甚至是某種合式公式的簡寫。
6. 符號相等：$\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$」代表變數可以與函數符號組成更一般的物件。據此形式，遞迴地規定一類合法詞彙——項為：

遞迴定義 — 

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

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

原子公式

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

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

這樣的形式。

公式

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

遞迴定義 — 

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

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

舉例來說，

$\{(\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)$

的重構過程如下

1. $\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \exists x[\lnot A_{2}^{1}(x)]$ （優先施用 $\lnot$）
2. $\{\lnot [\forall xA_{1}^{1}(x)]\}\Rightarrow \{\exists x[\lnot A_{2}^{1}(x)]\}$ （施用 $\exists$）
3. $\{\{\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》。根據上面語法一節，公式是由原子公式遞迴地添加邏輯連結詞而來的，而原子公式是由斷言符號與項所構成的。所以要檢定一條公式在特定的論域下正不正確，就要規定項的取值，然後檢定這樣的取值會不會落在斷言符號所對應的關係裡。由此延伸出所有公式的「真假值「。

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

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

通常一套解釋方法（簡稱為解釋）會以代號 $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}}$ 為假。

1. 若任意解釋下公式 ${\mathcal {B}}$ 都為真，稱 ${\mathcal {B}}$ 為邏輯有效的（logically valid） （類似於命題邏輯的恆真式）
2. 若一階邏輯理論 ${\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)$ 滿足：

1. ${\mathcal {C}}_{n}$ 符號辨識上為 ${\mathcal {A}}$。
2. 所有的 ${\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)$ 滿足：

1. ${\mathcal {C}}_{n}$ 符號辨識上為 ${\mathcal {A}}$。
2. 所有的 ${\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}}$

證明

（注意這是元邏輯下的證明）： 假設 ${\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}}$ ：

1. $\Gamma \vdash (\neg {\mathcal {A}})\Leftrightarrow (\neg {\mathcal {B}})$
2. $\Gamma \vdash ({\mathcal {C}}\Rightarrow {\mathcal {A}})\Leftrightarrow ({\mathcal {C}}\Rightarrow {\mathcal {B}})$
3. $\Gamma \vdash ({\mathcal {A}}\Rightarrow {\mathcal {C}})\Leftrightarrow ({\mathcal {B}}\Rightarrow {\mathcal {C}})$
4. 變數 $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)$

的話，添加的是常數符號 $c_{k}$ 與以下的新公理：

（$U$）${\mathcal {B}}(c_{k})$

添加常數符號的情況可視為添加函數符號情況的特例，因為常數符號可以視為「零變數」的函數符號。

但不管如何，還需假設 $f_{k}^{n}$ 和新理論的邏輯公理、量詞公理相容，也就是所有公理模式須涵蓋內含 $f_{k}^{n}$ 的項。特別像是（A4）這種將自由變數代換成項的公理模式，也就是說，若項 $T$ 內含 $f_{k}^{n}$ ，且公式 ${\mathcal {D}}(x)$ 內自由的 $x$ 都不在 $T$ 的變數的量詞範圍內，那

$\forall x{\mathcal {D}}(x)\Rightarrow {\mathcal {D}}(T)$

仍然是新理論的公理。

另外還需要考慮到 $f_{k}^{n}$ 與等號的相容性（換句話說，新理論仍須是帶等號的一階邏輯理論），這樣的話，考慮到上面等式定理所述的條件（E2''），需額外假設：

新理論的額外假設 — 
對任何介於 $1$ 與 $n$ 的下標 $k$ 和變數 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$

$(t_{k}=x)\Rightarrow [\,f_{k}^{n}(t_{1},\,\ldots ,\,t_{k},\,\ldots ,\,t_{n})=f_{k}^{n}(t_{1},\,\ldots ,\,x,\,\ldots ,\,t_{n})\,]$

是公理 （若是添加常數符號的特例，就不須額外假設以上的公理）

這樣就有以下直觀的定理

元定理 — 
對變數 $t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x$ 有

（E）$\vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Leftrightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)$

證明

（$\Rightarrow$） $\vdash _{n}[\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （1）$(y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,]$ （E2） （2）$(\forall y)\{(y=x)\Rightarrow [\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},y)\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\,]\}$ （GEN with 1, $y$） （3）$[\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow \{\,{\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\,\}$ （MP with A4, 2） （4）$[\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})=x\,]\Rightarrow {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （D2 with $U^{\prime }$, 3） （$\Leftarrow$） $\vdash _{n}{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},x)\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （1）$\forall x\forall y\{\,[\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,y)\,]\Rightarrow (x=y)\,\}$ （MP with AND and $U$） （2）$\forall x{\big \{}\,\{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,{\big \}}$ （A4 with 1 and $y$） （3）$\{\,{\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]\,\}\Rightarrow [\,x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （A4 with 2 and $x$） （4）${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)$ （Hyp） （5）${\mathcal {B}}(t_{1},\,t_{2},\,\ldots ,\,t_{n},\,x)\wedge {\mathcal {B}}[\,t_{1},\,t_{2},\,\ldots ,\,t_{n},\,f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})\,]$ （AND with $U$ and 4） （6）$x=f_{k}^{n}(t_{1},\,t_{2},\,\ldots ,\,t_{n})$ （MP with 3 and 5）

換句話說，「 $s=0$ 」在新理論裡等價於 「對所有的實數 $r\in \mathbb {R}$ ， $r+s=r$」。

一階邏輯的元定理

下面列出了一些重要的元邏輯定理。

1. 不像命題演算，一階邏輯是不可判定性的。對於任意的公式P，可以證實沒有判定過程，判定P是否有效，（參見停機問題）。（結論獨立的來自於邱奇和圖靈。）
2. 有效性的判定問題是半可判定的。按哥德爾完備性定理所展示的，對於任何有效的公式P, P是可證明的。
3. 一元斷言邏輯（就是說，斷言只有一個參數的斷言邏輯）是可判定的。

轉換自然語言到一階邏輯

用自然語言表達的概念必須在一階邏輯（FOL）可以為為其效力之前必須被轉換到FOL，而在這種轉換中可能有一些潛在的缺陷。在FOL中，$p\lor q$意味著「要麼p要麼q要麼二者」，就是說它是「包容性」的。在英語中，單詞「or」有時是包容性的（比如，「加牛奶或糖？」），有時是排斥性的（比如，「喝咖啡或茶？」，通常意味著取其中一個或另一個但非二者）。類似的，英語單詞「some」可以意味著「至少一個，可能全部」，有時意味著「不是全部，可能沒有」。英語單詞「and」有時要按「or」轉換（比如，「男人和女人可以申請」）。

一階邏輯的限制

所有數學概念都有它的強項和弱點；下面列出一階邏輯的一些問題。

難於表達if-then-else

帶有等式的FOL不包含或允許定義if-then-else斷言或函數if（c,a,b），這裡的c是表達為公式的條件，而a和b是要麼都是項要麼都是公式，並且它的結果是a如果c為真，或者b如果它為假。問題在於FOL中，斷言和函數二者只接受（「非布林類型」）項作為參數，而條件的明確表達是（「布林類型」）公式。這是不幸的，因為很多數學函數是依據if-then-else而方便的表達的，而if-then-else是描述大多數電腦程式的基礎。

在數學上，有可能重定義匹配公式算子的新函數的完備集合，但是這是非常笨拙的。 斷言if（c,a,b）如果重寫為$(c\wedge a)\lor (\neg c\wedge b)$就可以在FOL中表達，但是如果條件c是複雜的這就是笨拙的。很多人擴充FOL增加特殊情況斷言叫做「if（條件，a, b）」（這裡a和b是公式）和／或函數「ite（條件，a, b）」（這裡的a和b是項），它們都接受一個公式作為條件，並且等於a如果條件為真，或b如果條件為假。這些擴充使FOL易於用於某些問題，並使某類自動定理證明更容易。 其他人進一步擴充FOL使得函數和斷言可以在任何位置接受項和公式二者。

類型（種類）

除了在公式（「布林類型」）和項（「非布林類型」）之間的區別之外，FOL不包括類型（種類）到自身的概念中。 某些人爭辯說缺乏類型是巨大優點 ，而很多其他人發覺了定義和使用類型（種類）的優點，比如幫助拒絕某些錯誤或不想要的規定 。 想要指示類型的那些人必須使用在FOL中可獲得的符號來提供這種資訊。這麼做使得這種表達更加複雜，並也容易導致錯誤。

單一參數斷言可以用來在合適的地方實現類型的概念。例如：

$\forall x(Man(x)\rightarrow Mortal(x))$，

斷言Man（x）可以被認為是一類「類型斷言」（就是說，x必須是男人）。 斷言還可以同指示類型的「存在」量詞一起使用，但這通常應當轉而與邏輯合取算子一起來做，比如：

$\exists x(Man(x)\wedge Mortal(x))$（「存在既是男人又是人類的事物」）。

容易寫成$\exists xMan(x)\rightarrow Mortal(x)$，但這將等價與$\exists x\neg Man(x)\lor \exists xMortal(x)$（「存在不是男人的事物或者存在是人類的事物」），這通常不是想要的。類似的，可以做一個類型是另一個類型的子類型的斷言，比如：

$\forall x(Man(x)\rightarrow Mammal(x))$（「對於所有x，如果x是男人，則x是哺乳動物）。

難於刻畫模型大小

主條目：二階邏輯

從Löwenheim–Skolem定理得出在一階邏輯中不可能刻畫有限性或可數性。若一階理論有任意有限大的模型，則也有無窮大的模型，所以說不能刻劃有限性。而若理論有某個無窮基數大小的模型，則也必有任意更大的模型，所以不能刻劃可數性。另一個例子，是無法用一階語言將實數系公理化，因為不論用何種一階理論描述，既然該理論有實數系此種無窮模型（大小為$2^{\aleph _{0}}$），所以必有比實數系更大（比如$2^{2^{\aleph _{0}}}$）的另一個模型，從而該理論不是（唯一地）刻劃實數系的性質。實數系滿足的公理中，有上確界性質一項，它聲稱實數的所有有界的、非空集合都有上確界。一階邏輯祗能對元素量化，但此公理中，要對模型的全部子集量化，這就需要二階邏輯了。

圖可及性不能表達

很多情況可以被建模為節點和有向連接（邊）的圖。例如，效驗很多系統要求展示不能從「好」狀態觸及到「壞」狀態，而狀態的相互連接經常可以建模為圖。但是，可以證明這種可及性不能用斷言邏輯完全表達。換句話說，沒有斷言邏輯公式f，帶有u和v作為它的唯一自由變數，而R作為它唯一的（2元）斷言符號，使得f在一個有向圖中成立，如果在這個圖中存在從關聯於u的節點到關聯於v的節點的路徑。

參見

• 真值表
• 邏輯等價
• 邏輯條件
• 邏輯與非
• 邏輯或非
• 數理邏輯
• 零階邏輯
• 一階語言
• 二階邏輯
• 布林函數
• 推理規則列表
• 哥德爾完備性定理
• 哥德爾不完備定理

參考文獻

來源

• Jon Barwise and John Etchemendy，2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
• David Hilbert and Wilhelm Ackermann 1950. Principles of Theoretical Logic（English translation）. Chelsea. The 1928 first German edition was titled Grundzüge der theoretischen Logik.
• Wilfrid Hodges, 2001, "Classical Logic I: First Order Logic", in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

外部連結

• Stanford Encyclopedia of Philosophy：＂Classical Logic（頁面存檔備份，存於網際網路檔案館） -- by Stewart Shapiro. Covers syntax, model theory, and metatheory for first order logic in the natural deduction style.
• forall x: an introduction to formal logic（頁面存檔備份，存於網際網路檔案館）, by P.D. Magnus, covers formal semantics and proof theory for first-order logic.
• Metamath（頁面存檔備份，存於網際網路檔案館）：an ongoing online project to reconstruct mathematics as a huge first order theory, using first order logic and the axiomatic set theory ZFC. Principia Mathematica modernized and done right.
• Podnieks, Karl. Introduction to mathematical logic.（頁面存檔備份，存於網際網路檔案館）