一阶逻辑
一阶逻辑是使用於数学、哲学、语言学及電腦科學中的一种形式系统，也可以稱為：一阶斷言演算、低階斷言演算、量化理論或谓词逻辑。一階邏輯和命題邏輯的不同之處在於，一階邏輯包含量詞。
高階邏輯和一階邏輯不同之處在於，高階邏輯的斷言符號可以有斷言符號或函數符號當做引數，且容許斷言量詞或函數量詞。在一階邏輯的語義中，斷言被解釋為關係。而高階邏輯的語義裡，斷言則會被解釋為集合的集合。
在通常的語義下，一階邏輯是可靠（所有可證的敘述皆為真）且完備（所有為真的敘述皆可證）。雖然一階邏輯的邏輯歸結只是半可判定性的，但還是有許多用於一階邏輯上的自動定理證明。一階邏輯也符合一些使其能通過證明論分析的元邏輯定理，如勒文海姆–斯科倫定理及緊緻性定理。
一階邏輯是數學基礎中很重要的一部份。許多常見的公理系統，如一階皮亞諾公理、冯诺伊曼-博内斯-哥德尔集合论和策梅洛-弗蘭克爾集合論都是一階理論。然而一階邏輯不能控制其無窮模型的基數大小，因根據勒文海姆–斯科倫定理和康托爾定理，可以構造出一種"病態"集合論模型，使整個模型可數，但模型內卻會覺得自己有「不可數集」。類似地，可以證明實數系的普通一階理論既有可數模型又有不可數模型。這類的悖論被稱為斯科倫悖論。但一階的直覺主義邏輯裡，勒文海姆–斯科倫定理不可證明，故不會有以上之現象
以下通俗的介紹一階邏輯。
在命題邏輯裡，「蘇格拉底是哲學家」、「柏拉圖是哲學家」只能簡單標記為 formula_1 及 formula_2 。
而在一階邏輯，我們先將符號 formula_3 解釋為 「 formula_4 是哲學家」，然後以 formula_5 代表蘇格拉底； formula_6 代表柏拉圖，則 formula_7 對應到 formula_1 ； formula_9 對應到 formula_2 。也就是我們賦予斷言符號「formula_3 」語意的解釋，而這個解釋預設一個「所有人類的群體」(也就是我們一階邏輯語義的論域)，將變數 formula_4 解釋為從這個群體取出來討論的一個人。
事實上斷言符號可以包含不只一個的變數，比如說我們可以把 formula_13 解釋為「"x"與"y"是夫妻」，這樣 就可以解釋為「蘇格拉底和"y"是夫妻」。
進一步的，斷言符號和變數還可以和邏輯符號組合成更複雜的敘述。例如將斷言符號 formula_15 解釋為 formula_4 為學者。則「若"x"為哲學家，則"x"為學者」可以表示為
而「對所有"x"，若"x"為哲學家，則"x"為學者」之類的敘述，我們寫為 也就是自左方開始閱讀，以 formula_19 代表「對所有"x"」；將敘述理解為「對所有的"x"， formula_19 右方的敘述為真。」而 formula_19 這個符號我們稱為 formula_4 的全稱量詞
但全稱量詞直觀上，會有「若所有"x"是哲學家，那"x"的長子也會是哲學家」這樣的敘述，為此我們將formula_23 解釋為 「"x"的長子」，這樣前面的敘述可以寫為 這種解釋為成與 formula_4 有唯一對應的那個對象的符號，稱為函數符號。而事實上這段直觀為真的敘述，經過適當的擴展以後就是一階邏輯其中的一條公理。
而對於「有"x"是哲學家」，我們引入另一種量詞而表記為： 自左方開始閱讀，以 formula_27代表「存在"x"」；也就是解釋為「有"x"使 formula_27 右方的敘述為真」。而 formula_27 被稱為 formula_4 的存在量詞。全稱量詞和存在量詞一起被簡稱為量詞
而直觀上，「並非所有"x"不是哲學家」，和「有"x"是哲學家」是等價的；且「並非有"x"不是學者」也跟「所有的"x"是學者」在直觀上也是等價的。所以只要有「否定」這個邏輯概念，那一階邏輯就只需要一種量詞。據此，並且為了使邏輯公理的敘述更加簡潔，一般會以全稱量詞為基礎，作以下的符號定義( formula_31 解釋為 「否定」， 而 formula_32 代表一段"敘述")： 而將存在量詞定義為全稱量詞的衍伸符號。
在通常的一階邏輯語意解釋上，需要一個量詞所提及物件所組成的非空集合，稱為論域。例如，formula_34為真的意思為，若論域裡有物件使斷言Phil為真。也就是嚴格來說，通常的一階邏輯語義需要一套集合論基礎，但一般的嚴謹的公理化集合論都是以一階邏輯的語言來敘述（如策梅洛-弗蘭克爾集合論）。這不免讓一階邏輯語義淪為"具有集合論公理的一階邏輯理論的一套"，用來有效的檢驗一段"敘述"(合式公式)是否為這個一階邏輯理論的定理。
一階邏輯的形式理論可分成幾個部份： 一套理論到底能容許多少符號，取決於人類以物理定律的手段能塑造和容下多少的符號。但以目前所知是無法確知宇宙是不是有限，或是是否可無限制分割。雖然所有的公理化集合論都以量詞的形式隱晦的承認無窮的存在(如ZF集合論的無窮公理)，甚至以這樣自然數意義上的無窮為基礎，去建構出不可數的實數。但將之對應到現實，還是會遇到同樣的物理問題。
謹慎起見，以下各種類的符號沒有特別聲明，數量將會是有限個。
詞彙表中存在若干個邏輯符號，通常包括：注意並非所有的符號都需要，比如說比較極端的理論，因謝費爾豎線(或異或)的布林代數完備性使得所有不含量詞的邏輯公理可以以謝費爾豎線表述，而大幅減少基礎的邏輯聯結詞。
另外，一些作者並沒有將語義學和形式理論劃分清楚，而會將真值常數納入符號的一環；用T、V"pq"或formula_55來表示「真」，並用F、O"pq"或formula_56來表示「假」。
「他們兩人是夫妻」，代表一個關於兩個"對象"的斷言，而「他是人」、「三點共線」顯示了斷言是容許一個──甚至多個對象，所以對於自然數 formula_57 、formula_58 我們約定： 為一階邏輯的合法詞彙，它在直觀上表示一個有 formula_57 個"對象"的斷言，我們稱它為 formula_57 元斷言符號。下標的自然數 formula_58 只是拿來和其他同為 formula_57 元的斷言符號作區別。
實用上只要有申明，不至於和其他詞彙引起混淆的話，我們可以用任意的形式簡寫一個斷言符號，如公理化集合論裡的 formula_64 就是一個雙元斷言符號，也可以用 formula_65 冗長地表達。
「物體的顏色」、「夫妻的長子」說明了一列對象所唯一對應的對象。但不同的夫妻有不同的長子；不同的物體有不同的顏色，所以對於自然數 formula_57 、formula_58 我們約定： 為一階邏輯的合法詞彙，它在直觀上表示 formula_57 個"對象"所對應到的東西，我們稱它為 formula_57 元函數符號。但特別注意這種＂唯一對應＂的直觀想法，必須配上關於"等式"的性質(詳見下面等式定理)，才能被實現。
就像斷言符號，不引起混淆的話我們可以用任何的形式簡寫函數符號，如公理化集合論裡的 formula_71 是依據聯集公理而定義的新函數符號(請參見下面「函數符號與唯一性」的章節)，也可以冗長的表記為 formula_72 。
「刻度0」、「原點」、「蘇格拉底」這種(至少在作者的)直觀上"唯一不變"的對象，使我們對自然數 formula_58 約定 為一階邏輯的合法詞彙，它在直觀上表示一個"唯一不變"的對象。稱為常數符號，同樣的"常數的不變"需配上關於"等式"的性質(詳見下面等式定理)才能被實現。
為了不和變數的表記混淆，常數符號一樣可以用任何的形式簡寫，如公理化集合論裡的 formula_75 是根據空集公理和「函數符號與唯一性」的章節，而定義的新常數符號。亦可冗長的表示為 formula_74 。
和自然語言(如英語)不同，一階邏輯的語言以明確的遞迴定義判斷一個給定的詞彙是否合法。大致上來說，一階邏輯以「項」代表討論的對象，而對「項」的斷言組成了最基本的原子(合式)公式；而原子公式和邏輯符號組成了更複雜的合式公式(也就是"敘述")。
「那對夫妻的長子的職業」、「formula_77」、「formula_78」代表變數可以與函數符號組成"更一般的物件"，為此我們遞迴地規定一類合法詞彙——項為：
我們習慣用大寫的西方字母(如英文字母、希伯來字母、希臘字母)代表項，如果變數不得不採用大寫字母，而跟會項引起混淆的話，需額外規定分辨的辦法。
為了比較簡潔的規定甚麼是合式公式，我們先規定原子公式為：（若 formula_79 是項） 這樣的形式。
一階邏輯的合式公式（簡稱公式或 formula_81 ）以下面的規則遞迴地定義：
另外成對的中括弧跟大括弧，符號辨識上我們視為成對的小括弧。我們習慣以草書的大寫西方字母為公式的代號。
舉例來說， 是公式而 則不是公式。
而接下來我們只要對任意公式formula_32 、 formula_85 與變數 formula_4，做以下符號定義
這樣所有的邏輯連接詞與量詞就納入了合式公式的規範。
所謂的施用/作用，是以下公式形式的口語說法：(其中 formula_32 與 formula_85 都是公式)就好似運算子作用在它們身上。
量詞所施用的公式被稱為量詞的範圍(scope)。同一個變數在公式一般來說不只出現一次，若變數 formula_4 某次出現在 formula_19 的範圍內，稱這樣出現的 formula_4 為不自由/被約束的 formula_4 (not free/bounded)；反過來說，不出現在 formula_19 的範圍內的某個 formula_4 被稱為自由的 formula_4。
例如，對於公式： formula_122 就是量詞 formula_19 的範圍；而formula_124 裡的 formula_4 就是不自由的；反之 formula_126 裡的 formula_127 就是自由的。
說 formula_4 於公式 formula_32 完全自由，意為於 formula_32 出現的 formula_4 都是自由的；反之，說 formula_4 於公式 formula_32 完全不自由/完全被約束，意為 formula_32 內根本沒有 formula_4 ，或是 formula_32 內沒有自由的 formula_4 。若 formula_32 內所有的變數都完全不自由，formula_32 特稱為封閉公式/句子(closed formula/sentence)。
括弧是為了保證語意解釋符合預期，但太多的括弧書寫不易，為此我們規定以下的"重構法"(反過來就是"簡寫法")，從表面上不合法的一串符號找出作者原來想表達的公式：
舉例來說 的重構過程如下
可以被重構為公式的一串符號，我們寬鬆的認定為"合式公式"。(最明顯的例子就是合式公式最外層的括弧可以"省略")
波蘭表示法將邏輯連接詞前置於被施用的公式而非傳統的中間。如果沿用以上的"施用順序"，這個表示法允許捨棄所有括弧。如公式 轉成波蘭表示法的過程如下
對於公式 formula_32 和 formula_85： 直觀意義非常明顯，就是"p"=>"q"且"p"可以推出"q"。
它们实际上是公理模式，代表著"跟自然數一樣多"條的公理。
以下的 formula_4 為任意變數， formula_85 、 formula_158 為任意公式。
它们实际上是公理模式。
根據不同作者的看法，甚至是理論本身的需求，「等式」在形式理論裡可能是斷言符號或是一段公式(如"a"等於"b"可定義為對所有的"x"，"x"屬於"a"等價於"x"屬於"b")。而如何刻劃直觀上「等式的性質」，有一開始就將「等式的性質」視為公理(模式)，但也有視為的另一套處理方法，以下暫且以公理模式的方式處理。以元定理處理的方法會在等式定理詳述。 事實上這兩個公理模式也確保了函數符號＂唯一對應＂和常數符號的＂唯一性＂，但證明這些性質需要一些元定理，簡便起見我們合併於等式定理一節講述。
一階邏輯的標準語義源於波蘭邏輯學家Alfred Tarski所著《On the Concept of Truth in Formal Languages》。根據上面語法一節，公式是由原子公式遞迴地添加邏輯連結詞而來的，而原子公式是由斷言符號與項所構成的。所以要檢驗一條公式在特定的論域下正不正確，就要規定項的取值，然後檢驗這樣的取值會不會落在斷言符號所對應的關係裡。由此延伸出所有公式的＂真假值＂。
也就是一套一階邏輯的語義解釋，要包含 通常一套解釋方法(簡稱為解釋)會以代號 formula_159 表示。
量詞的解釋需要指明變數取值範圍的論域——也就是一個集合 formula_160 。而變數可能跟自然數一樣多，換句話說，所有變數在論域 formula_160 取的值可以依序以自然數標下標——也就是一個在 formula_160 取值的數列。如果我們以 formula_163 的代號(不一定是變數本身的表示符號)來列舉變數，那麼從 formula_160 的某套變數取值就以
或較直觀的符號
來表示。
一套解釋 formula_159 會將 formula_57 元函數符號 formula_169 解釋成某個 formula_170 的 formula_57 元函數；而常數符號 formula_172 解釋成特定的 formula_173 (亦稱為 formula_172 的取值為 formula_175)，這樣就可以用上面語法一節定義項的方式，遞迴地規定項的取值： 直觀上要解釋關係最直接的方法，就是列舉所有符合關係的對象；例如如果想說明夫妻關係，可以列舉所有 (老公, 老婆) 的雙元有序對，但並非所有的人類有序對都會在這個關係中。
以此為基礎，若以 formula_176 代表所有以 formula_177 個 formula_160 中的元素構成的 formula_177 元有序對的集合(也就是 formula_177 元笛卡兒積) ，那一套解釋 formula_159 會將 formula_177 元斷言符號 formula_183 解釋為一個 的formula_177 元有序對子集合。
這樣就可以依據語法的遞迴定義，以下面的規則對每條公式賦予真值。(這種賦值方式稱為T-模式，取名於邏輯學家Alfred Tarski)
更進一步的來說 另一種一階邏輯語義的方法可經由命題邏輯的林登鮑姆-塔斯基代數擴展而成。有如下幾種類型： 這些代數都是純粹擴展兩元素布林代數而成的格。
塔斯基和葛范德於1987年證明，沒有超過包在三個以上的量化內的原子句子的部份一階邏輯，其表示力和關係代數相同。上述部份一階邏輯令人十分地感到有興趣，因為它已足夠表示皮亞諾算術和公理化集合論，包括典型的ZFC。他們亦證明了，具有簡單有序對的一階邏輯和具有兩個有序的投影函數的關係代數等價。
上述的語義解釋都要求論域為非空集合。但在如自由邏輯之中，設定空論域是被允許的。甚至代數結構的類包含一個空結構（如空偏序集），當允許空論域時，這個類只能是一階邏輯中的一個基本類，不然就要將空結構由類中移除。
不過，空論域存在著一些難點： 因此，若空論域是被允許的，通常也必須被視成特例。不過，大多數的作家會簡單地將空論域由定義中排除。
以下介紹一些基本用語和符號
口語上會稱公式 formula_32 (或 formula_190 ) 為 formula_191 下的定理(theorem)。而這列formula_192 會稱為formula_190 的證明。
例如定理formula_194 formula_195的證明： 上面事實上蘊含了無限多定理的證明。方便起見，這種還是會以表示定理的方法來表示。
直觀上的證明，總是會有一些"前提假設"，對此，若我們以 formula_196 代表一列有限數目的公式，那
這樣我們稱 formula_192 為在前提 formula_196 下， formula_32 的證明；或是說 formula_32 是 formula_196 的推論結果。
若要特別凸顯 formula_196 裡的一條"前提條件" formula_85 對"證明過程"的重要性，可以用 formula_204 的符號去特別凸顯。若 formula_196 裡的公式列舉出來有 formula_206 ，那亦可表示為 證明過程沒有被引用的公式，我們盡量不會寫出來。另一方面從以上對於證明定義可以發現，依怎樣的順序列舉前提條件，對於證明本身是不會有任何影響的。
本節所介紹的符號，在引用哪個理論很顯然的情況下，formula_208 的下標formula_191 可以省略。
實際的證明常常會"引用"別的(元)定理，嚴格來說，就是照抄(元)定理的證明過程，然後作一些修改使符號一致。為了節省證明的篇幅，引用時只會單單列出配合引用(元)定理所得出的公式(形式)，並在後面註明引用的(元)定理代號。
從公理(A1)和(A2)會得出不但直觀且實用的演繹元定理：
因為 formula_196 代表的是有限條公式，所以透過演繹元定理可以將證明過程必要的前提條件遞迴地移到 formula_211 後，直到不需要任何前提為止；然後由MP律可以知道，若有 formula_212 ，則有 formula_213，如此一來透過演繹元定理搬到推論結果的合式公式，也可以任意的搬回來。所以 formula_214 等價於某定理 formula_215 。因此我們也會將 formula_214 稱為一個定理。 而從演繹元定理和MP律，我們會有以下直觀且實用的元定理 以下如果需要將引用的定理以演繹元定理進行"搬移"，會省略掉搬移的過程並在搬移後得到的結果後標註(D)。如果引用以上的(D1)和(D2)也會省略過程，單有結果和代號標註。
上面兩定理表達了雙否定推理上等價於於原公式，引用兩者任一會都以(DN)簡寫。
以上二定理表說明 formula_217 推理上等價於 formula_218 ，引用這兩個定理中任一都以(T)表示。
以下的定理重現了實質條件的直觀理解。
以下的元定理和公理模式(A3)間只差了一個否定，故以(A3')標示。
我們有"且"的交換性
類似的，(C2)正是"或"的"可交換性"：
"且"的直觀意義是實質條件元定理的直接結果
從(AND)和 formula_48 的符號定義可知，formula_220 的證明可以拆成兩部分；習慣上我們會以「( formula_42 ) 」標示 formula_222 部分的證明，而「( formula_223 ) 」標示 formula_224 部分的證明。
類似的，"或"的直觀意義是(M0)跟(D)的直截結果
以下的定理則是(A3')的直截結果
對於"且"，展開符號定義後，可以從直觀意義輕鬆地得到
"或"也有類似的性質
"且"和"或"之間還有分配律
以下的元定理的名字來自於英國邏輯學家奧古斯塔斯·德摩根。
公理模式(A7)可以稍加延伸成以下的元定理 更進一步，有以下元定裡 (GEN)可以稍加修飾，以套用在含有存在量詞的公式上
由普遍化，很容易證明以下關於"交換性"的定理 注意最後(3)一般來說是不能反向的，只要想到"對每個 formula_225，都有一個數(也就是 formula_226 )，使 formula_227"，但是任取一個 formula_225 的數 formula_229 和任意的數 formula_6 ， formula_231 並不一定會為零。 一般來說，formula_232 會被視為某個 formula_233 的簡寫(包括視為斷言符號)。若使用元定理的形式刻劃等式的性質，會作如下的定義 上面的定義符合函數符號直觀上的＂唯一對應＂。為了證明常數符號的＂唯一性＂，我們需要以下元定理
從上面可以得知，如果等式符號僅僅為斷言符號，那等式和它的公理一節的等式公理模式，是等價於本節的(E1)+(E2')+(E2")。
由上面的元定理，對帶有等式符號的 formula_191 可以證明以下的等式性質
對任意常數符號 formula_235 ，上列元定理確保了 也就是常數符號的＂唯一性＂。
下面列出了一些重要的元逻辑定理。
用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到FOL，而在这种转换中可能有一些潜在的缺陷。在FOL中，formula_238意味着“要么p要么q要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖？”），有时是排斥性的（比如，“喝咖啡或茶？”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。 所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。
带有等式的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）如果重写为formula_239就可以在FOL中表达，但是如果条件c是复杂的这就是笨拙的。很多人扩展FOL增加特殊情况斷言叫做“if（条件，a, b）”（这里a和b是公式）和／或函数“ite（条件，a, b）”（这裡的a和b是项），它们都接受一个公式作为条件，并且等于a如果条件为真，或b如果条件为假。这些扩展使FOL易于用于某些问题，并使某类自动定理证明更容易。 其他人进一步扩展FOL使得函数和斷言可以在任何位置接受项和公式二者。
除了在公式（“布尔类型”）和项（“非布尔类型”）之间的区别之外，FOL不包括类型（种类）到自身的概念中。 某些人争辩说缺乏类型是巨大优点 ，而很多其他人发觉了定义和使用类型（种类）的优点，比如帮助拒绝某些错误或不想要的规定 想要指示类型的那些人必须使用在FOL中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。
单一参数斷言可以用来在合适的地方实现类型的概念。例如： 斷言Man(x)可以被认为是一类“类型断言”（就是说，x必须是男人）。 斷言还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如： 容易写成formula_242，但这将等价与formula_243（“存在不是男人的事物或者存在是人类的事物”），这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如：
从Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。若一階理論有任意有限大的模型，則也有無窮大的模型，所以說不能刻劃有限性。而若理論有某個無窮基數大小的模型，則也必有任意更大的模型，所以不能刻劃可數性。另一個例子，是無法用一階語言將實數系公理化，因為不論用何種一階理論描述，既然該理論有實數系此種無窮模型（大小為formula_245），所以必有比實數系更大（比如formula_246）的另一個模型，從而該理論不是（唯一地）刻劃實數系的性質。實數系滿足的公理中，有上确界性质一項，它声称实数的所有有界的、非空集合都有上确界。一階邏輯祗能對元素量化，但此公理中，要對模型的全部子集量化，这就需要二阶逻辑了。
很多情况可以被建模为节点和有向连接（边）的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用斷言逻辑完全表达。换句话说，没有斷言逻辑公式f，带有u和v作为它的唯一自由变量，而R作为它唯一的（2元）斷言符号，使得f在一个有向图中成立，如果在这个图中存在从关联于u的节点到关联于v的节点的路径。