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

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

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

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

簡介 
在命題邏輯裡，「蘇格拉底是哲學家」、「柏拉圖是哲學家」只能簡單標記為  及  。

而一階邏輯先设符號  意為 「 x 是哲學家」，然後以  代表蘇格拉底、  代表柏拉圖，則  對應  ；  對應  。也就是賦予斷言符號「 」語意的解釋。這個解釋預設一個「所有人類的群體」（也就是語義解釋的論域），并將變數  解釋為自群體中取出來的某人。

斷言符號可以包含一個以上的變數。例如：设  意為「 x 與 y 是夫妻」，则  意为「蘇格拉底和 y 是夫妻」。

一階邏輯和命題邏輯相同，斷言符號和變數還能與邏輯符號組成更複雜的敘述。例如：设斷言符號  意為  是學者。則「若 x 為哲學家，則 x 為學者」可表示為：

而「對所有 x ，若 x 為哲學家，則 x 為學者」則記為：

也就是自左方開始閱讀，以  表示「对于所有 x 」，可以將之理解為「对于所有 x ，  右方的敘述為真。」其中， 這個符號被称为  的全稱量詞。

直觀上有「若所有x是哲學家，那x的長子也會是哲學家」這樣“合理”的敘述。若设  意為 「 x 的長子」，那么這段“合理”敘述可記為：

 表示“與  有唯一對應的那個對象”，被稱為函數符號。這段直觀為真的敘述，經過適當的擴展以後就是一階邏輯其中的一條公理。

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

自左方開始閱讀，以  代表「存在 x 」，可以將之理解為「有 x 使  右方的敘述為真」。其中， 被稱為  的存在量詞。全稱量詞和存在量詞一起被簡稱為量詞。

直觀上，「並非所有 x 不是哲學家」，和「有 x 是哲學家」是等價的；且「不存在 x 不是學者」也与「所有的 x 是學者」等價。所以只要有「否定」這個邏輯概念，那么一階邏輯就能以全稱量詞為基礎，作以下的符號定義（  解釋為 「否定」， 而  代表一段＂敘述＂）：

由此，存在量詞被定義為全稱量詞的衍伸。

形式理論 
一階邏輯的形式理論可分成幾個部份：
：決定哪些符號組合是合式公式。（直觀上的“文法無誤的敘述”）
推理規則：由合式公式符號組合出新合式公式的規則（直觀上的“推理”）
公理：一套合式公式（直觀上的基本假設）

基本符號 
一套理論能容許多少符號，取決於人類根据物理定律能塑造多少符號。但以目前無法確知宇宙是不是有限，或是是否可無限制分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認無窮的存在（如ZF集合論的無窮公理），甚至以這樣自然數意義上的無窮為基礎，去建構出不可數的實數。但將之對應到現實，還是會回到同樣的物理問題。

謹慎起見，以下各種類的符號沒有特別聲明，數量將會是有限個。

邏輯符號 
詞彙表中存在若干個邏輯符號，通常包括：

量化符號  及 
某些作者會把  符號定義為 ，如此便只需要  做為基礎符號。
邏輯聯結詞：以下為可能的表示符號（关于波蘭表示法下的邏輯連接詞，請參見逻辑运算的波兰记法）：
否定：  或  
條件： 或  或 
且： 或  
或： 或 ||
雙條件： 或 
某些作者會作如下的符號定義：

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

注意：並非所有的符號都是必需的。比如，在比較極端的情况中，因为謝費爾豎線（或異或）的布林代數完備性使得所有不含量詞的邏輯公理都可以用謝費爾豎線表述，而大幅減少基礎的邏輯聯結詞。

另外，一些作者並沒有將語義學和形式理論劃分清楚，而會將真值常數納入符號的一環：用 T 、Vpq 或  來表示「真」，並用 F 、 Opq 或  來表示「假」。

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

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

實用上只要有申明，不至於和其他詞彙引起混淆的話，可以用任意的形式簡寫一個斷言符號。如：公理化集合論裡的雙元斷言符號  也可以表示为  。

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

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

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

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

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

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

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

項 
「那對夫妻的長子的職業」、「」、「」代表變數可以與函數符號組成更一般的物件。據此形式，遞迴地規定一類合法詞彙——項為：
變數和常數是項。
若  全都是項，那么  也是項。
項只能通过以上兩點，於有限步驟內建構出來。
習慣上以大寫的西方字母（如英文字母、希伯來字母、希臘字母）代表項，如果變數不得不採用大寫字母，而可能跟項引起混淆的話，需額外規定分辨的辦法。

原子公式 
為了比較簡潔地規定甚麼是合式公式，先規定原子公式為：（若  是項）
 
這樣的形式。

公式 
一階邏輯的合式公式（簡稱公式或  ）以下面的規則遞迴地定義：
原子公式為公式。（美觀起見，在原子公式外面包一層括弧也是公式）
若  為公式，則  為公式。
若  與  為公式，則  為公式。
若  為公式，  為任意變數，則  為公式。 （美觀起見 ，也就是裡面的量詞有無外包括弧都是公式）
合式公式只能通过以上四點，於有限步驟內建構出來。
另外成對的中括弧跟大括弧，符號辨識上視為成對的小括弧，而草書的大寫西方字母為公式的代號。

舉例來說，

是公式而

則不是公式。

而接下來只要對任意公式 、  與變數 ，做以下符號定義
 （同樣美觀起見 ）
這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。

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

 稱為  施用於  上。
 稱為  施用於  和  上。
 稱為  施用於  和  上。 
 稱為  施用於  和  上。 
 稱為  施用於  和  上。 
 稱為  施用於  上。 
 稱為  施用於  上。

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

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

例如，對於公式：

 就是量詞    的範圍；而  裡的  就是不自由的；反之  裡的  就是自由的。

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

括弧的簡寫 
括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此規定以下的“重構法”（反過來就是“簡寫法”），從表面上不合法的一串符號找出作者原來想表達的公式：
若整串符號的括弧不成對，直接視為無法重構。
以（左至右）的施用順序重構括弧。
相鄰的邏輯連接詞或量詞無法決定施用順序的話，以右邊為先。
重構施用的順序，以被成對括弧包住的部分為優先施用，其次才是落單的斷言符號。

舉例來說

的重構過程如下
 （優先施用 ）
 （施用 ）
 （最後施用 ）

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

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

轉成波蘭表示法的過程如下
 （轉成波蘭表示法的順序）
 （邏輯連結詞的符號轉換）

推理规则

MP律 
對於公式  和 ：
 和  組合出 。
直觀意義非常明顯，就是p=>q且p可以推出q。

公理

邏輯公理 
如果、、都是公式，則：
（A1） 
（A2） 
（A3） 
都是公理。
它们实际上是公理模式，代表著“跟自然數一樣多”條的公理。

量词公理 
以下的  為任意變數，  、  為任意公式。
（A4）  是一個項，  為  中出現的任意變數；若  裡，所有  的的範圍裡都沒有自由的  （這個情況稱為  裡項  對  是自由的），則

為公理
其中  代表把  裡自由的  都取代為  所得到的新公式。
（A5）如果  在  裡完全被約束，則

為公理
（A6）  為公理
（A7） 若  是公理，  是任意變數，則

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

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

 是一段變數  、  完全自由，且型式完全被確定的公式  的簡寫。要求：
（E1） 對任意變數  ，  為公理。
（E2） 對於任意變數  和 ，若在公式  中自由的  都不在  的範圍內。若以 代表  某些（而非全部）自由的   被取代成  而成的新公式，則
 
為公理。
事實上這兩個公理模式也確保了函數符號“唯一對應”和常數符號的“唯一性”，但證明這些性質需要一些元定理，簡便起見合併於下面的等式定理一節講述。

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

也就是一套一階邏輯的語義解釋，要包含
變數取值的論域
如何解釋函數符號（為論域中的某個函數）與常數符號（為論域中的某特定元素），以便從特定的變數取值得出項的取值。
如何將斷言符號與論域裡的某關係做對應。
通常一套解釋方法（簡稱為解釋）會以代號  表示。

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

或較直觀的符號

來表示。

一套解釋  會將  元函數符號  解釋成某個  的  元函數；而常數符號  解釋成特定的  （亦稱為  的取值為 ），這樣就可以用上面語法一節定義項的方式，遞迴地規定項的取值：
在解釋  下的某套變數取值下，一列項  的取值分別為 ，則這套變數取值下，項  的取值規定為

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

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

的 元有序對子集合。

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

反之

則定義為假。
在一套特定的變數取值下，「 為真」 等價於 「 為假」。
在一套特定的變數取值下， 為真，意為「  為假或是  為真。」 （p=>q為假只有p為真且q為假的狀況）
在變數取值  下， 為真，意為「對所有的  ，  於變數取值  下為真」。（也就是把變數  的取值換為論域的任意元素仍然為真）
更進一步的來說
在一套解釋  下，不管怎麼樣的變數取值，公式  都為真，則稱為  下  為真，以符號  簡記。若沒有變數取值可以滿足  ，則稱  下  為假。
若任意解釋下公式  都為真，稱  為邏輯有效的（logically valid） （類似於命題邏輯的恆真式）
若一階邏輯理論  的公理都於  為真，稱解釋  為  之模型（model）

代數化語義 
另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型：
圓柱代數，由阿爾弗雷德·塔斯基和其同事提出；
多元代數，由保羅·哈爾莫斯提出。
斷言函子邏輯，主要是基於威拉德·范·奧曼·奎因的工作成果。
這些代數都是純粹擴展兩元素布林代數而成的格。

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

空論域 

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

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

常用的推理性質

定理與證明 
以下介紹一些基本用語和符號
在一階邏輯理論  下，   代表有一列公式  滿足：
  符號辨識上為 。
所有的 有下列兩種可能情況
 為  的公理。
存在 使得  為  （也就是由前面的公式以MP律組合出來）
口語上會稱公式  （或  ） 為  下的定理（theorem）。而這列 會稱為 的證明。

例如定理  的證明：
： （公理A2）
： （公理A1）
： （公理A1）
： （和加上MP律）
： （和加上MP律）

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

直觀上的證明，總是會有一些“前提假設”，對此，若以  代表一列有限數目的公式，那 
 代表有一列公式  滿足：
  符號辨識上為 。
所有的  有下列三種可能情況
 為  的公理。
 為  中的其中一條公式。
存在 使得  為  （也就是由前面的公式以MP律組合出來）
這樣稱  為在前提  下，  的證明；或是說  是  的推論結果。

若要特別凸顯  裡的一條＂前提條件＂  對＂證明過程＂的重要性，可以用  的符號去特別凸顯。若  裡的公式列舉出來有  ，那亦可表示為

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

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

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

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

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

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

（D2） 

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

否定 
（DNe） Double negation, elimination
（DNi） Double negation, introduction

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

（T1） Transposition-1
（T2） Transposition-2

以上二定理表說明  推理上等價於  ，引用這兩個定理中任一都以（T）表示。

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

（A3'）

實質條件 
以下的定理重現了實質條件的直觀理解。
（M0）material condition

 

（也就是）

（M1）material condition

（M2）material condition

（M3）material condition

反證法 
（C1）Proof by Contradiction

（C2）Proof by Contradiction

證明提示：仿（C1）。

邏輯與和邏輯或

交換性 

以下為＂且＂的交換性

類似的，（C2）正是＂或＂的＂可交換性＂：

 （C2, D）

直觀意義 

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

（AND）Intuitive meaning of And：

 （M1）

 （M3）

 （M2）

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

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

（OR）Intuitive meaning of OR：

 （M0, DN）

 （A1, D）

 （D）

 （交換性, D）

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

（DisJ）Disjunction：

結合律 

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

（ASO-AND）Associativity of AND：

證明提示： （AND）

＂或＂也有類似的性質

（ASO-OR）Associativity of OR

證明提示： （M1）, （M2）, （M3）

分配律 

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

（DIS-1）Distribution：

（DIS-2）Distribution：

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

De Morgan II：

證明

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

對任意變數  ，若  則有 。

更進一步，有以下元定裡
元定理（普遍化, GEN）：

在  裡變數  都完全被約束，若

則有

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

元定理（GENe）：

若變數  在  的公式和  裡都完全被約束則

（1） 若  則 

（2） 若  則 

證明提示：對（GEN）使用（T）和（A5）

量詞的可交換性 
由普遍化，很容易證明以下關於＂交換性＂的定理
（1） 

（2） 

（3） 

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

量詞的簡寫 
數學中常常有 ＂對所有  有...＂，或是 ＂存在  使的...＂。而兩句話比較清晰，接近一階邏輯語言的說法是 ＂對所有  ，只要  則...＂ 與  ＂存在  ，  且...＂。「大於」直觀上是一個二元关系，也就是說，在公理化集合論裡對應於一條  （ 或  ） 在裡面完全自由的合式公式。據此，可做以下的符號定義如果變數  和  都於合式公式  裡完全自由，那
但直觀上也會說 ＂對所有  和  有...＂，這樣連續，帶有條件的全稱量詞也是有＂交換性＂的。 為了討論這個問題，首先需要一些前置的定理（abb） 這樣就可以證明以下定理如果變數  和  都於合式公式  和  裡完全自由，若項  裡沒有  那
如果再加上 ＂項  裡沒有  ＂ 那就是 ＂對所有  和  有...＂，也就是以上所討論的情況了。以這個定理配上全稱量詞本身的交換性定理，那這句話就可以等價的說成 ＂對所有  和  若   且   則...＂，所以根據＂且＂的可交換性，可以進一步的說成 ＂對所有  和  有...＂，所以連續帶有條件的全稱量詞是＂可交換的＂。也就是說如果變數  和  都於合式公式  和  裡完全自由，若項  裡沒有  ，且項  裡沒有  則
但對於存在量詞，仿造上面的證明過程，只能得出以下非等價的定理。這是因為一般來說，  不總是能推出  。所以帶有條件的存在量詞是沒有交換性的。

等式定理 
一般來說，等式  會被視為某個合式公式  的簡寫。若使用元定理的形式刻劃等式的性質，會作如下的定義
說一階邏輯理論  帶相等符號  意為（  、  和  都是  的任意變數）
除了變數  和  於  是完全自由外其他變數都完全被約束
（E1）  。
（E2'）  為  內不含函數符號與常數符號的原子公式 ， 若以  表示  內某一個  被取代成  而成的新公式，則有

（E2＂） 若以  代表項  裡的  被取代成  而成的新項，則有

（E3）  。
並在這種狀況下，規定  為  的簡寫。

上面的定義符合函數符號直觀上的＂唯一對應＂。為了證明常數符號的＂唯一性＂，需要以下元定理
說一階邏輯理論  帶相等符號  ，等同於要求：
 除了變數  和  於  是完全自由外其他變數都完全被約束。
符合（E1）。
（E2） 對於任意變數  和 ，若在公式  中自由的  都不在  的範圍內。若以 代表  某些（而非全部）自由的   被取代成  而成的新公式，則
從上面可以得知，如果等式符號僅僅為斷言符號，那等式和它的公理一節的等式公理模式，是等價於本節的（E1）+（E2'）+（E2＂）。

由上面的元定理，對帶有等式符號的  可以證明以下的等式性質
若  、  與  為  的任意項，則有
 
 
 
證明提示：
（E1）+（GEN）+（A4）。
將  帶入（E2）後使用（D2），然後套用兩次（GEN）+（A4）即可。
注意到從（E2）有 ，然後套用三次（GEN）+（A4）即可。
對任意常數符號  ，上列元定理確保了

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

函數符號與唯一性

一阶逻辑的元定理 

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

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

类型（种类） 

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

单一参数斷言可以用来在合适的地方实现类型的概念。例如：
，
斷言Man（x）可以被认为是一类“类型断言”（就是说，x必须是男人）。
斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如：
（“存在既是男人又是人类的事物”）。
容易写成，但这将等价与（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：
（“对于所有x，如果x是男人，则x是哺乳动物）。

难于刻画模型大小 

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

图可及性不能表达 

很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式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.

Y
形式逻辑系统