一阶逻辑

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

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

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

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

簡介

基本符號

命題邏輯顧名思義，會將「蘇格拉底是哲學家」、「柏拉圖是哲學家」之類直觀上有真有假的敘述簡記為 $p$ 及 $q$ （也就是有真有假的命題），然後討論 $\mathrm{\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 是夫妻」。

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

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

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

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

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

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

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

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

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

$\mathrm{\exists }x𝒜:=\mathrm{\neg }[\mathrm{\forall }x(\mathrm{\neg }𝒜)]$

相等

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

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

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

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

形式理論

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

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

基本符號

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

邏輯符號

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

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

   $𝒜\wedge ℬ:=\mathrm{\neg }(𝒜\Rightarrow (\mathrm{\neg }ℬ)),$

   $𝒜\vee ℬ:=(\mathrm{\neg }𝒜)\Rightarrow ℬ,$

   $𝒜\iff ℬ:=(𝒜\Rightarrow ℬ)\wedge (ℬ\Rightarrow 𝒜),$

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

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

並非所有的符號都不可或缺的，像謝費爾豎線「$|$」（或異或）可以用來定義量詞以外的所有邏輯符號，換句話說： Template:Math theorem 另外，一些作者不區分語義解釋和形式理論，所以會將表示真值的符號納入形式理論裡，也就是說，用 T 、Vpq 或 $\mathrm{\top }$ 來表示「真」，並用 F 、 Opq 或 $\mathrm{\perp }$ 來表示「假」。

斷言符號

「他們兩人是夫妻」，是一個關於兩個“對象”的斷言，而「他是人」、「三點共線」则表明斷言容許一個或者多個對象。所以對於自然數 $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$ 是項）

$A_j^n(T_1,....,T_n)$

這樣的形式。

公式

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

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

舉例來說，

$\{(\mathrm{\forall }y)A_1^2[x,f_1^1(y)]\}$

是公式而

$\mathrm{\forall }xx\Rightarrow$

則不是公式。

而接下來只要對任意公式$𝒜$ 、 $ℬ$ 與變數 $x$，做以下符號定義

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

施用

所謂的施用/作用，是以下公式形式的口語說法：（其中 $𝒜$ 與 $ℬ$ 都是公式）

• $(\mathrm{\neg }𝒜)$ 稱為 $\mathrm{\neg }$ 施用於 $𝒜$ 上。
• $(𝒜\Rightarrow ℬ)$ 稱為 $\Rightarrow$ 施用於 $𝒜$ 和 $ℬ$ 上。
• $(𝒜\wedge ℬ)$ 稱為 $\wedge$ 施用於 $𝒜$ 和 $ℬ$ 上。
• $(𝒜\vee ℬ)$ 稱為 $\vee$ 施用於 $𝒜$ 和 $ℬ$ 上。
• $(𝒜\iff ℬ)$ 稱為 $\iff$ 施用於 $𝒜$ 和 $ℬ$ 上。
• $(\mathrm{\forall }x𝒜)$ 稱為 $\mathrm{\forall }x$ 施用於 $𝒜$ 上。
• $(\mathrm{\exists }x𝒜)$ 稱為 $\mathrm{\exists }x$ 施用於 $𝒜$ 上。

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

自由變數和約束變數

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

例如，對於公式：

$\{(\mathrm{\forall }x)[A_1^1(x)\Rightarrow A_2^1(y)]\}$

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

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

括弧的簡寫

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

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

舉例來說

$\mathrm{\neg }[\mathrm{\forall }x{A}_1^1(x)]\Rightarrow \mathrm{\exists }x\mathrm{\neg }{A}_2^1(x)$

的重構過程如下

1. $\{\mathrm{\neg }[\mathrm{\forall }x{A}_1^1(x)]\}\Rightarrow \mathrm{\exists }x[\mathrm{\neg }{A}_2^1(x)]$ （優先施用 $\mathrm{\neg }$）
2. $\{\mathrm{\neg }[\mathrm{\forall }x{A}_1^1(x)]\}\Rightarrow \{\mathrm{\exists }x[\mathrm{\neg }{A}_2^1(x)]\}$ （施用 $\mathrm{\exists }$）
3. $\{\{\mathrm{\neg }[\mathrm{\forall }x{A}_1^1(x)]\}\Rightarrow \{\mathrm{\exists }x[\mathrm{\neg }{A}_2^1(x)]\}\}$ （最後施用 $\Rightarrow$）

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

波蘭表示法

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

$\mathrm{\forall }x\mathrm{\forall }y\{A_1^1[f_1^1(x)]\Rightarrow \mathrm{\neg }\{A_1^1(x)\Rightarrow A_1^3[f_1^1(y),x,z]\}\}$

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

$\mathrm{\forall }x\mathrm{\forall }y\Rightarrow A_1^1{f}_1^{1}x\mathrm{\neg }\Rightarrow A_1^{1}x{A}_1^3{f}_1^{1}yxz$ （轉成波蘭表示法的順序）

$\mathrm{\Pi }x\mathrm{\Pi }y\text{C}{A}_1^1{f}_1^{1}x\text{N}\text{C}{A}_1^{1}x{A}_1^3{f}_1^{1}yxz$ （邏輯連結詞的符號轉換）

推理规则

一階邏輯通常只有以下的推理規則（因為將普遍化視為推理規則會有不直觀的限制） Template:Math theorem 直觀意義非常明顯，就是p=>q且p可以推出q。

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

公理

邏輯公理

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

在有（A1）與（A2）的前提下，（A3）等價於以下的公理模式：（證明請參見下面否定一節。） Template:Math theorem 另外，在只以謝費爾豎線「$|$」為基礎邏輯連接詞的公理系统裡，上面三條公理模式等價於下面這條公理模式： Template:Math theorem

量词公理

Template:Math theorem 它们实际上也是公理模式。

等式和它的公理

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

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

標準語義

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

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

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

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

項的取值

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

${⟨a_k⟩}_{k\in \mathbb{N}}$

或較直觀的符號

$⟨a_1,a_2,a_3,\cdots ⟩$

來表示。

一套解釋 $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$），這樣就可以用上面語法一節定義項的方式，遞迴地規定項的取值： Template:Math theorem

真假的賦值

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

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

${(A_j^m)}^M\subseteq D^m$

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

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

代數化語義

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

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

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

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

空論域

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

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

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

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

常用的推理性質

定理與證明

以下介紹一些基本用語和符號 Template:Math theorem 口語上會稱公式 $𝒜$ （或 ${⊢}_{ℒ}𝒜$ ） 為 $ℒ$ 下的定理（theorem）。而這列${𝒞}_i(1\le i\le n)$ 會稱為${⊢}_{ℒ}𝒜$ 的證明。

例如定理$(I)$ ${⊢}_{ℒ}ℬ\Rightarrow ℬ$ 的證明：

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

直觀上的證明，總是會有一些“前提假設”，對此，若以 $\mathrm{\Gamma }$ 代表一列有限數目的公式，那 Template:Math theorem 這樣稱 ${𝒞}_i(1\le i\le n)$ 為在前提 $\mathrm{\Gamma }$ 下， $𝒜$ 的證明；或是說 $𝒜$ 是 $\mathrm{\Gamma }$ 的推論結果。

若要特別凸顯 $\mathrm{\Gamma }$ 裡的一條＂前提條件＂ $ℬ$ 對＂證明過程＂的重要性，可以用 $\mathrm{\Gamma },ℬ{⊢}_{ℒ}𝒜$ 的符號去特別凸顯。若 $\mathrm{\Gamma }$ 裡的公式列舉出來有 ${ℬ}_1,...,{ℬ}_n$ ，那亦可表示為

${ℬ}_1,...,{ℬ}_n{⊢}_{ℒ}𝒜$

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

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

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

演繹元定理

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

證明

（注意這是Template:Link-en下的證明）： 假設 ${𝒞}_1,{𝒞}_2,....,{𝒞}_n$ 為條件所說 $𝒞$ 的證明，如果 ${𝒞}_1$ 是$\mathrm{\Gamma }$ 裡的公式或 $ℒ$ 的公理，那根據（A1） $⊢{𝒞}_1\Rightarrow (ℬ\Rightarrow {𝒞}_1)$ 所以由MP律有 $\mathrm{\Gamma }⊢ℬ\Rightarrow {𝒞}_1$ 若 ${𝒞}_1$ 是 $ℬ$，那因為 $⊢ℬ\Rightarrow ℬ$ 所以有 $\mathrm{\Gamma }⊢ℬ\Rightarrow {𝒞}_1$ 至此${𝒞}_1$的部分證明完畢。 接下來要用歸納法；假設對 $i<k$ 都有 $\mathrm{\Gamma }⊢ℬ\Rightarrow {𝒞}_i$ 。 若${𝒞}_k$ 是公理、或從 $\mathrm{\Gamma }$ 來的、或是根本就是 $ℬ$，仿造上面 ${𝒞}_1$ 的部分就有 $\mathrm{\Gamma }⊢ℬ\Rightarrow {𝒞}_k$ 剩下沒考慮的狀況是由MP律組合出 ${𝒞}_k$ 的狀況，也就是有 $l,m<k$ 使${𝒞}_m$ 是 ${𝒞}_l\Rightarrow {𝒞}_k$。 由公理A2有 $⊢[ℬ\Rightarrow ({𝒞}_l\Rightarrow {𝒞}_k)]\Rightarrow [(ℬ\Rightarrow {𝒞}_l)\Rightarrow (ℬ\Rightarrow {𝒞}_k)]$ 套用歸納法的假設，加上MP律，就會發現 $\mathrm{\Gamma }⊢ℬ\Rightarrow {𝒞}_k$ 如此可以一路歸納到 ${𝒞}_n$ 也就是 $𝒞$ 的情況，故元定理得證。$◻$

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

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

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

否定

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

證明（使用A3）

（1）$(\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)\Rightarrow [(\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }𝒜)\Rightarrow 𝒜]$ （A3） （2）$\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }𝒜$ （I） （3）$(\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)\Rightarrow 𝒜$ （D2 with 1, 2） （4）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow (\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)$ （A1） （5）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜$ （D1 with 3, 4）

證明（使用T1）

（1）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow (\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)$ （A1） （2）$\mathrm{\neg }\mathrm{\neg }𝒜$ （Hyp） （3）$\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （MP with 2, 1） （4）$\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜$ （MP with 3, T1） （5）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜$ （MP with 4, T1） （6）$𝒜$ （MP with 2, 5）

證明（使用A3）

（1）$(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }𝒜)\Rightarrow [(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜)\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜]$ （A3） （2）$(\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜)\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （MP with DNe, 1） （3）$𝒜\Rightarrow (\mathrm{\neg }\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜)$ （A1） （4）$𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （D1 with 2,3）

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

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

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

證明（使用T1）

（1）$\mathrm{\neg }\mathrm{\neg }ℬ\Rightarrow ℬ$ （DN） （2）$ℬ\Rightarrow 𝒜$ （Hyp） （3）$\mathrm{\neg }\mathrm{\neg }ℬ\Rightarrow 𝒜$ （D with 1, 2） （4）$𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （DN） （5）$\mathrm{\neg }\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （D1 with 3,4） （6）$(\mathrm{\neg }\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)\Rightarrow (\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }ℬ)$ （T1, D） （7）$\mathrm{\neg }𝒜\Rightarrow \mathrm{\neg }ℬ$ （MP with 5, 6）

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

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

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

（T1）可推出（A3）的證明

由MP律顯然有 $\mathrm{\neg }ℬ,(\mathrm{\neg }ℬ\Rightarrow ℬ)⊢ℬ$ （1）$\mathrm{\neg }ℬ\Rightarrow [(\mathrm{\neg }ℬ\Rightarrow ℬ)\Rightarrow ℬ]$ （對上面的定理使用兩次演繹元定理） （2）$\mathrm{\neg }ℬ\Rightarrow [\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }(\mathrm{\neg }ℬ\Rightarrow ℬ)]$（D1 with 1, T2） （3）$(\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }ℬ)\Rightarrow [\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }(\mathrm{\neg }ℬ\Rightarrow ℬ)]$（MP with A2, 2） （4）$\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }(\mathrm{\neg }ℬ\Rightarrow ℬ)$（MP with I, 3） （5）$(\mathrm{\neg }ℬ\Rightarrow ℬ)\Rightarrow ℬ$（MP with T1, 4） （6）$(\mathrm{\neg }ℬ)\Rightarrow (\mathrm{\neg }𝒞)$（Hyp） （7）$\mathrm{\neg }ℬ\Rightarrow 𝒞$（Hyp） （8）$\mathrm{\neg }𝒞\Rightarrow \mathrm{\neg }\mathrm{\neg }ℬ$（MP with T2, 7） （9）$\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }ℬ$（D1 with 6, 8） （10）$\mathrm{\neg }ℬ\Rightarrow ℬ$（D1 with DN, 9） （11）$ℬ$（MP with 5, 10）

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

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

證明

（1）$(\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)\Rightarrow [(\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜)\Rightarrow ℬ]$ （A3） （2）$(\mathrm{\neg }𝒜\Rightarrow ℬ)\Rightarrow (\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜)$ （T, D） （3）$\mathrm{\neg }𝒜\Rightarrow ℬ$ （Hyp） （4）$\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （MP with 2, 3） （5）$(\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜)\Rightarrow ℬ$ （MP with 1, 4） （6）$(𝒜\Rightarrow ℬ)\Rightarrow (\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜)$ （T, D） （7）$𝒜\Rightarrow ℬ$ （Hyp） （8）$\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜$ （MP with 6, 7） （9）$ℬ$ （MP with 5, 8）

實質條件

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

證明

（1）$\mathrm{\neg }𝒜$ （Hyp） （2）$𝒜$ （Hyp） （3）$(\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜)\Rightarrow [(\mathrm{\neg }ℬ\Rightarrow 𝒜)\Rightarrow ℬ]$ （A3） （4）$\mathrm{\neg }𝒜\Rightarrow (\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜)$ （A1） （5）$\mathrm{\neg }ℬ\Rightarrow \mathrm{\neg }𝒜$ （MP with 4, 1） （6）$𝒜\Rightarrow (\mathrm{\neg }ℬ\Rightarrow 𝒜)$ （A1） （7）$\mathrm{\neg }ℬ\Rightarrow 𝒜$ （MP with 6, 2） （8）$(\mathrm{\neg }ℬ\Rightarrow 𝒜)\Rightarrow ℬ$ （MP with 3,5） （9）$ℬ$ （MP with 8,7）

證明

首先注意到$𝒜,𝒜\Rightarrow ℬ⊢ℬ$ （MP） （1）$𝒜\Rightarrow [(𝒜\Rightarrow ℬ)\Rightarrow ℬ]$ （0, D） （2）$[(𝒜\Rightarrow ℬ)\Rightarrow ℬ]\Rightarrow \{\mathrm{\neg }ℬ\Rightarrow [\mathrm{\neg }(𝒜\Rightarrow ℬ)]\}$ （T） （3）$𝒜$ （Hyp） （4）$(𝒜\Rightarrow ℬ)\Rightarrow ℬ$ （MP with 1, 3） （5）$\mathrm{\neg }ℬ\Rightarrow [\mathrm{\neg }(𝒜\Rightarrow ℬ)]$ （MP with 2, 4） （6）$\mathrm{\neg }ℬ$ （Hyp） （7）$\mathrm{\neg }(𝒜\Rightarrow ℬ)$ （MP 5, 6）

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

證明

（1）$\mathrm{\neg }𝒜\Rightarrow (𝒜\Rightarrow ℬ)$ （M0, D） （2）$[\mathrm{\neg }𝒜\Rightarrow (𝒜\Rightarrow ℬ)]\Rightarrow \{[\mathrm{\neg }(𝒜\Rightarrow ℬ)]\Rightarrow (\mathrm{\neg }\mathrm{\neg }𝒜)\}$ （T） （3）$[\mathrm{\neg }(𝒜\Rightarrow ℬ)]\Rightarrow (\mathrm{\neg }\mathrm{\neg }𝒜)$ （MP with 1, 2） （4）$\mathrm{\neg }(𝒜\Rightarrow ℬ)$ （Hyp） （5）$\mathrm{\neg }\mathrm{\neg }𝒜$ （MP with 3,4） （6）$𝒜$ （MP with 5, DN）

反證法

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

邏輯與和邏輯或

且與或的交換性

以下為邏輯與的交換性

證明

（1）$(ℬ\Rightarrow \mathrm{\neg }𝒜)\Rightarrow (𝒜\Rightarrow \mathrm{\neg }ℬ)$ （C1, D） （2）$[(ℬ\Rightarrow \mathrm{\neg }𝒜)\Rightarrow (𝒜\Rightarrow \mathrm{\neg }ℬ)]\Rightarrow \{[\mathrm{\neg }(𝒜\Rightarrow \mathrm{\neg }ℬ)]\Rightarrow [\mathrm{\neg }(ℬ\Rightarrow \mathrm{\neg }𝒜)]\}$ （T, D） （3）$[\mathrm{\neg }(𝒜\Rightarrow \mathrm{\neg }ℬ)]\Rightarrow [\mathrm{\neg }(ℬ\Rightarrow \mathrm{\neg }𝒜)]$ （MP with 1,2）

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

且與或的直觀意義

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

從（AND）和 $\iff$ 的符號定義可知，$⊢ℬ\iff 𝒞$ 的證明可以拆成兩部分；習慣上會以「（ $\Rightarrow$ ） 」標示 $⊢ℬ\Rightarrow 𝒞$ 部分的證明，而「（ $\Leftarrow$ ） 」標示 $⊢𝒞\Rightarrow ℬ$ 部分的證明。

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

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

證明
（1） $\mathrm{\neg }𝒜\Rightarrow ℬ$ （Hyp） （2） $ℬ\Rightarrow 𝒞$ （Hyp） （3） $\mathrm{\neg }𝒜\Rightarrow 𝒞$ （D1 with 1, 2） （4） $𝒜\Rightarrow 𝒞$ （Hyp） （5） $𝒞$ （A3' with 3, 4）

且與或的結合律

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

＂或＂也有類似的性質

且與或的分配律

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

證明

（$\Rightarrow$） （1）$𝒜\wedge (ℬ\vee 𝒞)$ （Hyp） （2）$𝒜$ （MP with 1, AND） （3）$\mathrm{\neg }ℬ\Rightarrow 𝒞$ （MP with 1, AND） （4）$\mathrm{\neg }\mathrm{\neg }(𝒜\Rightarrow \mathrm{\neg }ℬ)$ （Hyp） （5）$𝒜\Rightarrow \mathrm{\neg }ℬ$ （MP with 4, DN） （6）$𝒜\Rightarrow 𝒞$ （D1 with 3, 5） （7）$𝒞$ （MP with 2, 5） （8）$𝒜\wedge 𝒞$ （MP twice with 2, 7, AND） 也就是 $𝒜\wedge (ℬ\vee 𝒞),\mathrm{\neg }(𝒜\wedge ℬ)⊢𝒜\wedge 𝒞$ 再套用（D）就會得到 $𝒜\wedge (ℬ\vee 𝒞)⊢(𝒜\wedge ℬ)\vee (𝒜\wedge 𝒞)$ （$\Leftarrow$） （1）$\mathrm{\neg }(𝒜\wedge ℬ)\Rightarrow 𝒜\wedge 𝒞$ （Hyp） （2）$\mathrm{\neg }(𝒜\wedge ℬ)\Rightarrow 𝒜$ （D1 with 1, AND） （3）$\mathrm{\neg }(𝒜\wedge ℬ)\Rightarrow 𝒞$ （D1 with 1, AND） （4）$\mathrm{\neg }𝒜\Rightarrow (𝒜\wedge ℬ)$ （MP with 2, C2） （5）$\mathrm{\neg }𝒞\Rightarrow (𝒜\wedge ℬ)$ （MP with 3, C2） （6）$\mathrm{\neg }𝒜\Rightarrow 𝒜$ （D1 with 4, AND） （7）$\mathrm{\neg }𝒞\Rightarrow ℬ$ （D1 with 4, AND） （8）$𝒜$ （A3' with 6, I） （9）$𝒜\wedge (ℬ\vee 𝒞)$ （MP twice with 7, 8, AND） 也就是 $(𝒜\wedge ℬ)\vee (𝒜\wedge 𝒞)⊢𝒜\wedge (ℬ\vee 𝒞)$

證明

（$\Rightarrow$） （1）$\mathrm{\neg }𝒜\Rightarrow (ℬ\wedge 𝒞)$（Hyp） （2）$\mathrm{\neg }𝒜\Rightarrow ℬ$ （D1 with 1, AND） （3）$\mathrm{\neg }𝒜\Rightarrow 𝒞$ （D1 with 1, AND） （4）$(𝒜\vee ℬ)\wedge (𝒜\vee 𝒞)$（MP twice with 2, 3,AND） 也就是 $𝒜\vee (ℬ\wedge 𝒞)⊢(𝒜\vee ℬ)\wedge (𝒜\vee 𝒞)$ （$\Leftarrow$） （1）$(\mathrm{\neg }𝒜\Rightarrow ℬ)\wedge (\mathrm{\neg }𝒜\Rightarrow 𝒞)$ （Hyp） （2）$\mathrm{\neg }𝒜\Rightarrow ℬ$ （MP with 1, AND） （3）$\mathrm{\neg }𝒜\Rightarrow 𝒞$ （MP with 1, AND） （4）$\mathrm{\neg }𝒜$ （Hyp） （5）$ℬ$ （MP with 2,4） （6）$𝒞$ （MP with 3,4） （7）$ℬ\wedge 𝒞$ （MP twice with 5, 6, AND） 也就是 $𝒜\wedge (ℬ\vee 𝒞),\mathrm{\neg }𝒜⊢ℬ\wedge 𝒞$ 再使用一次推論元定理會得到 $𝒜\wedge (ℬ\vee 𝒞)⊢𝒜\vee (ℬ\wedge 𝒞)$

德摩根定律

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

證明

（$\Rightarrow$） （1）$\mathrm{\neg }\mathrm{\neg }[𝒜\Rightarrow (\mathrm{\neg }ℬ)]$ （Hyp） （2）$𝒜\Rightarrow (\mathrm{\neg }ℬ)$ （MP with 1, DN） （3）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow 𝒜$ （DN） （4）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow (\mathrm{\neg }ℬ)$ （D1 with 2, 3） （$\Leftarrow$） （1）$\mathrm{\neg }\mathrm{\neg }𝒜\Rightarrow (\mathrm{\neg }ℬ)$ （Hyp） （2）$𝒜\Rightarrow \mathrm{\neg }\mathrm{\neg }𝒜$ （DN） （3）$𝒜\Rightarrow (\mathrm{\neg }ℬ)$ （D1 with 1, 2） （4）$\mathrm{\neg }\mathrm{\neg }[𝒜\Rightarrow (\mathrm{\neg }ℬ)]$ （MP with DN, 3）

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

普遍化元定理

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

證明

假設${𝒞}_1,{𝒞}_2,....,{𝒞}_n$ 就是 $ℬ$的證明，那 ${𝒞}_1$一定是公理，根據（A7）可以得到 $⊢(\mathrm{\forall }x){𝒞}_1$ 若對 $i<k$ 都有 $⊢(\mathrm{\forall }x){𝒞}_i$ ，如果 ${𝒞}_k$ 是公理的話顯然 $⊢(\mathrm{\forall }x){𝒞}_k$ 。 若有 $l,m<k$ 使得 ${𝒞}_m:{𝒞}_l\Rightarrow {𝒞}_k$ 那根據歸納法的假設跟（A6）有 $⊢(\mathrm{\forall }x){𝒞}_l\Rightarrow (\mathrm{\forall }x){𝒞}_k$ 上式配上 $⊢(\mathrm{\forall }x){𝒞}_l$ 就可以得到 $⊢(\mathrm{\forall }x){𝒞}_k$ 以此歸納到${𝒞}_n$ 也就是 $ℬ$，故本元定理得證。$◻$

更進一步，有以下元定裡 Template:Math theorem

證明

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

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

等價代換

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

證明

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

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

$(𝒜\wedge 𝒞):=\mathrm{\neg }[𝒜\Rightarrow (\mathrm{\neg }𝒞)]$

那如果假設 $⊢𝒜\iff ℬ$ ，就有：

• $⊢[𝒜\Rightarrow (\mathrm{\neg }𝒞)]\iff [ℬ\Rightarrow (\mathrm{\neg }𝒞)]$
• $⊢\mathrm{\neg }[𝒜\Rightarrow (\mathrm{\neg }𝒞)]\iff \{\mathrm{\neg }[ℬ\Rightarrow (\mathrm{\neg }𝒞)]\}$

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

量詞的可交換性

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

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

量詞的簡寫

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

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

證明
（$\Rightarrow$） $𝒜\Rightarrow (ℬ\Rightarrow 𝒞)⊢(𝒜\wedge ℬ)\Rightarrow 𝒞$ 注意到 （AND） $𝒜\wedge ℬ⊢𝒜$ （AND） $𝒜\wedge ℬ⊢ℬ$ 所以 $𝒜\Rightarrow (ℬ\Rightarrow 𝒞),𝒜\wedge ℬ⊢𝒞$ 再套上演繹元定理就可以得證。$◻$ （$\Leftarrow$） $(𝒜\wedge ℬ)\Rightarrow 𝒞⊢𝒜\Rightarrow (ℬ\Rightarrow 𝒞)$ 注意到 （AND） $𝒜,ℬ⊢𝒜\wedge ℬ$ 所以 $(𝒜\wedge ℬ)\Rightarrow 𝒞,𝒜,ℬ⊢𝒞$ 再套上演繹元定理就可以得證。$◻$

這樣就可以證明以下定理 Template:Math theorem

證明

（$\Rightarrow$） $[\mathrm{\forall }𝒜(x,T)][\mathrm{\forall }ℬ(y,S)]𝒞⊢\mathrm{\forall }x\mathrm{\forall }y\{[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow ℬ\}$ （1）$(\mathrm{\forall }x)\{𝒜(x,T)\Rightarrow (\mathrm{\forall }y)[ℬ(y,S)\Rightarrow 𝒞]\}$ （Hyp） （2）$𝒜(x,T)\Rightarrow (\mathrm{\forall }y)[ℬ(y,S)\Rightarrow 𝒞]$ （MP with 1, A4） （3）$𝒜(x,T)\Rightarrow [ℬ(y,S)\Rightarrow 𝒞]$ （D1 with 2, A4） （4）$[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow 𝒞$ （MP with abb, 3） （5）$\mathrm{\forall }x\mathrm{\forall }y\{[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow ℬ\}$ （GEN with 4 twice） （$\Leftarrow$） $\mathrm{\forall }x\mathrm{\forall }y\{[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow ℬ\}⊢[\mathrm{\forall }𝒜(x,T)][\mathrm{\forall }ℬ(y,S)]𝒞$ （1）$\mathrm{\forall }x\mathrm{\forall }y\{[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow ℬ\}$ （Hyp） （2）$[𝒜(x,T)\wedge ℬ(y,S)]\Rightarrow ℬ$ （MP with 2, A4 twice） （3）$𝒜(x,T)\Rightarrow [ℬ(y,S)\Rightarrow 𝒞]$ （MP with abb, 2） （4）$(\mathrm{\forall }y)\{𝒜(x,T)\Rightarrow [ℬ(y,S)\Rightarrow 𝒞]\}$ （GEN with 3） （5）$𝒜(x,T)\Rightarrow (\mathrm{\forall }y)[ℬ(y,S)\Rightarrow 𝒞]$ （MP with A5, 4） （6）$(\mathrm{\forall }x)\{𝒜(x,T)\Rightarrow (\mathrm{\forall }y)[ℬ(y,S)\Rightarrow 𝒞]\}$ （GEN with 5）

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

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

證明

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

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

等式定理

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

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

證明

（$\Rightarrow$） 從（E1）+（E2'）+（E2＂）+（E3）推出（E2）的過程分成幾個階段推廣（E2'） （1）含有常數符號的原子公式 取 $c_j$ 為任意常數符號。目標是證明：對一段含常數符號 $c_j$ 但不含任何函數符號的原子公式 $ℬ(x,x,c_j)$ ，若 $ℬ(x,y,c_j)$ 表 $ℬ(x,x,c_j)$ 裡某一個 $x$ 被取代為 $y$ 的新公式，則 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [ℬ(x,x,c_j)\Rightarrow ℬ(x,y,c_j)]$ （a） （a）證明過程如下： 取一個不曾在 $ℬ(x,y,c_j)$ 出現的變數 $z$。若以 $ℬ(x,x,z)$ 表示 $ℬ(x,x,c_j)$ 內的 $c_j$ 都被取代成 $z$ 的新公式，將之帶入 （E2'）有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [ℬ(x,x,z)\Rightarrow ℬ(x,y,z)]$ 對上式，以變數 $z$ 取（GEN）有 ${⊢}_{ℒ}\mathrm{\forall }z\{ℰ(x,y)\Rightarrow [ℬ(x,x,z)\Rightarrow ℬ(x,y,z)]\}$ （b） 但從（A4）有 ${⊢}_{ℒ}\mathrm{\forall }z\{ℰ(x,y)\Rightarrow [ℬ(x,x,z)\Rightarrow ℬ(x,y,z)]\}\Rightarrow \{ℰ(x,y)\Rightarrow [ℬ(x,x,c_j)\Rightarrow ℬ(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$ 所構成的新公式。那現在的目標是證明 ${⊢}_{ℒ}ℰ(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），只需要證明 ${⊢}_{ℒ}ℰ(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'） ${⊢}_{ℒ}ℰ(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） ${⊢}_{ℒ}ℰ(x,y)\Rightarrow ℰ(T_k,S)$ （e） 也就是對（c）以變數 $z$ 和 $z^{\prime }$ 連續兩次使用（GEN），然後連續兩次與（A4）以MP律配合會得到 ${⊢}_{ℒ}ℰ(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$ 為任意常數符號） ${⊢}_{ℒ}ℰ(x,y)\Rightarrow ℰ(x,y)$ （e0） ${⊢}_{ℒ}ℰ(x,y)\Rightarrow ℰ(c_j,c_j)$ （e0'） （e0）就只是（I）故顯然成立；另一方面，對（E1）使用（GEN）然後與（A4）配合就會有 ${⊢}_{ℒ}ℰ(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$ 的詳細過程，那歸納法的前提就是 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow ℰ(S_r,{S_r}^{\prime })$ 那對（E2＂）使用 $n$ 次（GEN），然後同樣與（A4）以MP律配合 $n$ 次有 ${⊢}_{ℒ}ℰ(S_r,{S_r}^{\prime })\Rightarrow ℰ[f_i^n(S_1,\cdots ,S_r,\cdots ,S_n),f_i^n(S_1,\cdots ,{S_r}^{\prime },\cdots ,S_n)]$ 也就是 ${⊢}_{ℒ}ℰ(S_r,{S_r}^{\prime })\Rightarrow ℰ(T_k,S)$ 故將上式與歸納前提套入（D1）就會有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow ℰ(T_k,S)$ 至此（e）已被歸納法證明。 （3）任意的公式 為了將（E2'）從任意原子公式推廣到任意公式，根據語法對公式的遞迴定義，要分別對公式裡的量詞和邏輯連接詞的數量做歸納。 假設 $ℬ(x,x)$ 為不含邏輯連接詞的任意公式： $ℬ(x,x)$ 沒有量詞的情況就只是（c）而已，故成立。 若假設對於量詞數量為 $l$ 的 $ℬ(x,x)$ 有（ $ℬ(x,y)$ 代表 $ℬ(x,x)$ 內某個自由的 $x$ 被取代成 $y$ 所成的新公式） ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [ℬ(x,x)\Rightarrow ℬ(x,y)]$ 首先注意到新增量詞的時候，不可以取 $\mathrm{\forall }x$ 或是 $\mathrm{\forall }y$ ，否則上面的自由取代就會完全被破壞。故取個不是 $x$ 也不是 $y$ 的任意變數 $z$ ，對上式使用（GEN），然後與（A6）、（A5）配合使用MP律有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [\mathrm{\forall }zℬ(x,x)\Rightarrow \mathrm{\forall }zℬ(x,y)]$ 上式也就是量詞數量為 $l+1$ 的狀況，而把（E2'）推廣到了不含邏輯連接詞的任意公式上。 接下來對不含「 $\Rightarrow$ 」的任意公式裡的「 $\mathrm{\neg }$ 」的數量做歸納： 「 $\mathrm{\neg }$ 」的數量為零的情況剛剛已經證明，不再贅述。 假設「 $\mathrm{\neg }$ 」的數量為 $l$ ，沒有「 $\Rightarrow$ 」的公式下（E2'）都對，那對「 $\mathrm{\neg }$ 」的數量為 $l$ 的 $ℬ(x,x)$ 有（特別注意到推廣的（E2'）也可以將 $ℬ(x,y)$ 裡唯一的$y$ 取代成 $x$） ${⊢}_{ℒ}ℰ(y,x)\Rightarrow [ℬ(x,y)\Rightarrow ℬ(x,x)]$ （f） 那根據（T）有 ${⊢}_{ℒ}[ℬ(x,y)\Rightarrow ℬ(x,x)]\Rightarrow [\mathrm{\neg }ℬ(x,x)\Rightarrow \mathrm{\neg }ℬ(x,y)]$ （g） 這樣對（f）和（g）套用（D1），結果再和（E3）套用（D1）一次就有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [\mathrm{\neg }ℬ(x,x)\Rightarrow \mathrm{\neg }ℬ(x,y)]$ （f） 上式也就「 $\mathrm{\neg }$ 」的數量為 $l+1$ 的情況，故把（E2'）推廣到了僅不含「 $\Rightarrow$ 」的任意公式上。 為了要推廣到任意的公式上，我要要對「 $\Rightarrow$ 」的數量做歸納： 「 $\Rightarrow$ 」的數量為零的情況剛剛已經證明，不再贅述。 假設「 $\Rightarrow$ 」的數量小於 $l$ 的公式下（E2'）都對，那對但數量合起來為 $l$ 的 $ℬ(x,x)$ 與 $𝒞(x,x)$ 就會滿足 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [ℬ(x,x)\Rightarrow ℬ(x,y)]$ （*） ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [𝒞(x,x)\Rightarrow 𝒞(x,y)]$ （**） 考慮到（D1）有 $ℬ(x,x)\Rightarrow 𝒞(x,x),𝒞(x,x)\Rightarrow 𝒞(x,y){⊢}_{ℒ}ℬ(x,x)\Rightarrow 𝒞(x,y)$ $ℬ(x,y)\Rightarrow ℬ(x,x),ℬ(x,x)\Rightarrow 𝒞(x,x){⊢}_{ℒ}ℬ(x,x)\Rightarrow 𝒞(x,y)$ 那配上（*）與（**）就有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow \{[ℬ(x,x)\Rightarrow 𝒞(x,x)]\Rightarrow [ℬ(x,x)\Rightarrow 𝒞(x,y)]\}$ ${⊢}_{ℒ}ℰ(x,y)\Rightarrow \{[ℬ(x,x)\Rightarrow 𝒞(x,x)]\Rightarrow [ℬ(x,y)\Rightarrow 𝒞(x,x)]\}$ 上兩式就是所有「 $\Rightarrow$ 」的數量為 $l+1$ 的情況，故把（E2'）推廣到了任意公式。 最後，取代 $n+1$ 個 $x$ 的狀況，就是取代 $n$ 後再取代一次。所以可以由歸納法，從推廣後的（E2'）推出（E2） （ $\Leftarrow$ ） 首先（E2'）顯然只是（E2）的特例；要得到（E2＂）只要注意到由（E2）有 ${⊢}_{ℒ}ℰ(x_k,y)\Rightarrow \{ℰ[f_i^n(x_1,\cdots ,x_k,\cdots ,x_n),f_i^n(x_1,\cdots ,x_k,\cdots ,x_n)]\Rightarrow ℰ[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律有 ${⊢}_{ℒ}ℰ[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）有 ${⊢}_{ℒ}ℰ(x,y)\Rightarrow [ℰ(x,x)\Rightarrow ℰ(y,x)]$ 那這樣對上式和（E1）套用（D2）就有（E3）

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

由上面的元定理，對帶有等式符號的 $ℒ$ 可以證明以下的等式性質 Template:Math theorem 對任意常數符號 $c$ ，上列元定理確保了

${⊢}_{ℒ}(c=c)$

$(x=c),(y=c){⊢}_{ℒ}(x=y)$

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

函數符號與唯一性

唯一性

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

「存在 $s\in ℝ$ 使的對所有的實數 $r\in ℝ$ ， $r+s=r$」且「對所有的 $s^{\prime },s\in ℝ$ 和所有 $r\in ℝ$，若 $r+s=r$ 且 $r+s^{\prime }=r$ 則 $s=s^{\prime }$ 」

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

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

新舊理論的等效條件

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

「對所有的實數 $r\in ℝ$ 有 $r+0=r$ 」

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

存在 $s\in ℝ$ 使「$r>s$ 且對所有的 $x\in ℝ$ ， $x+s=x$」

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

更一般的來說，如果新的一階邏輯理論，是在舊的理論增添一些新符號跟新公理（並額外要求新符號與舊公理相容），那為了讓新舊理論等效，對於任意新理論的合式公式 $𝒞$ ，都要有某條相應的舊理論公式 ${𝒞}^{\prime }$ 滿足以下條件： Template:Math theorem 從條件（2）事實上就可以推出「若 ${⊢}_o{𝒞}^{\prime }$ ，則有 ${⊢}_n𝒞$ 」，因為 ${⊢}_o{𝒞}^{\prime }$ 的話， 新理論只是擴張舊理論而沒改變舊理論固有的定理，所以有 ${⊢}_n{𝒞}^{\prime }$ ，但這樣根據條件（2）跟MP律就會有 ${⊢}_n𝒞$。所以條件（2）事實上是比「舊的對那新的也對」強的條件，但在之後的推導上（2）會比較方便。

預備定理

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

證明

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

新理論的假設

一般來說，如果變數 $t_1,t_2,\dots ,t_n,x$ 在 $ℬ(t_1,t_2,\dots ,t_n,x)$ 完全自由，且舊理論裡有：

（$U$）${⊢}_o\mathrm{\exists }!xℬ(t_1,t_2,\dots ,t_n,x)$

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

（$U^{\prime }$）$ℬ[t_1,t_2,\dots ,t_n,f_k^n(t_1,t_2,\dots ,t_n)]$

如果僅僅是：

${⊢}_o\mathrm{\exists }!xℬ(x)$

的話，添加的是常數符號 $c_k$ 與以下的新公理：

（$U$）$ℬ(c_k)$

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

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

$\mathrm{\forall }x𝒟(x)\Rightarrow 𝒟(T)$

仍然是新理論的公理。

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

這樣就有以下直觀的定理 Template:Math theorem

證明

（$\Rightarrow$） ${⊢}_n[x=f_k^n(t_1,t_2,\dots ,t_n)]\Rightarrow ℬ(t_1,t_2,\dots ,t_n,x)$ （1）$(y=x)\Rightarrow [ℬ(t_1,t_2,\dots ,t_n,y)\Rightarrow ℬ(t_1,t_2,\dots ,t_n,x)]$ （E2） （2）$(\mathrm{\forall }y)\{(y=x)\Rightarrow [ℬ(t_1,t_2,\dots ,t_n,y)\Rightarrow ℬ(t_1,t_2,\dots ,t_n,x)]\}$ （GEN with 1, $y$） （3）$[f_k^n(t_1,t_2,\dots ,t_n)=x]\Rightarrow \{ℬ[t_1,t_2,\dots ,t_n,f_k^n(t_1,t_2,\dots ,t_n)]\Rightarrow ℬ(t_1,t_2,\dots ,t_n,x)\}$ （MP with A4, 2） （4）$[f_k^n(t_1,t_2,\dots ,t_n)=x]\Rightarrow ℬ(t_1,t_2,\dots ,t_n,x)$ （D2 with $U^{\prime }$, 3） （$\Leftarrow$） ${⊢}_nℬ(t_1,t_2,\dots ,t_n,x)\Rightarrow [x=f_k^n(t_1,t_2,\dots ,t_n)]$ （1）$\mathrm{\forall }x\mathrm{\forall }y\{[ℬ(t_1,t_2,\dots ,t_n,x)\wedge ℬ(t_1,t_2,\dots ,t_n,y)]\Rightarrow (x=y)\}$ （MP with AND and $U$） （2）$\mathrm{\forall }x\{\{ℬ(t_1,t_2,\dots ,t_n,x)\wedge ℬ[t_1,t_2,\dots ,t_n,f_k^n(t_1,t_2,\dots ,t_n)]\}\Rightarrow [x=f_k^n(t_1,t_2,\dots ,t_n)]\}$ （A4 with 1 and $y$） （3）$\{ℬ(t_1,t_2,\dots ,t_n,x)\wedge ℬ[t_1,t_2,\dots ,t_n,f_k^n(t_1,t_2,\dots ,t_n)]\}\Rightarrow [x=f_k^n(t_1,t_2,\dots ,t_n)]$ （A4 with 2 and $x$） （4）$ℬ(t_1,t_2,\dots ,t_n,x)$ （Hyp） （5）$ℬ(t_1,t_2,\dots ,t_n,x)\wedge ℬ[t_1,t_2,\dots ,t_n,f_k^n(t_1,t_2,\dots ,t_n)]$ （AND with $U$ and 4） （6）$x=f_k^n(t_1,t_2,\dots ,t_n)$ （MP with 3 and 5）

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

一阶逻辑的元定理

下面列出了一些重要的元逻辑定理。

1. 不像命题演算，一阶逻辑是不可判定性的。对于任意的公式P，可以证实没有判定过程，判定P是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）
2. 有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式P, P是可证明的。
3. 一元斷言逻辑（就是说，斷言只有一个参数的斷言逻辑）是可判定的。

转换自然语言到一阶逻辑

用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，$p\vee 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)\vee (\mathrm{\neg }c\wedge b)$就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况斷言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这裡的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。 其他人进一步扩展FOL使得函数和斷言可以在任何位置接受项和公式二者。

类型（种类）

除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 ，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 。 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。

单一参数斷言可以用来在合适的地方实现类型的概念。例如：

$\mathrm{\forall }x(Man(x)\to Mortal(x))$，

斷言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。 斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：

$\mathrm{\exists }x(Man(x)\wedge Mortal(x))$（“存在既是男人又是人类的事物”）。

容易写成$\mathrm{\exists }xMan(x)\to Mortal(x)$，但这将等价与$\mathrm{\exists }x\mathrm{\neg }Man(x)\vee \mathrm{\exists }xMortal(x)$（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：

$\mathrm{\forall }x(Man(x)\to Mammal(x))$（“对于所有x，如果x是男人，则x是哺乳动物）。

难于刻画模型大小

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

图可及性不能表达

很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式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 LogicTemplate:Wayback -- by Stewart Shapiro. Covers syntax, model theory, and metatheory for first order logic in the natural deduction style.
• forall x: an introduction to formal logicTemplate:Wayback, by P.D. Magnus, covers formal semantics and proof theory for first-order logic.
• MetamathTemplate:Wayback：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.Template:Wayback