概況
一階邏輯相關書籍一階謂詞演算或一階邏輯（FOL）允許量化陳述的公式，比如"存在著 x，..." (x) 或 "對於任何 x，..." （砢），這裡的 x 是論域(domain of discourse)的成員。一階（遞歸）公理化理論是通過增加一階句子/斷定的遞歸可枚舉集合作為公理，可以被公理化為一階邏輯擴展的理論。這裡的"..."叫做謂詞並表達某種性質。謂詞是適用於某些事物的表達。所以，表達"是黃色"或"喜歡椰菜"分別適用於是黃色或喜歡椰菜的那些事物。
一階邏輯是區別於高階邏輯的數理邏輯，它不允許量化性質。性質是一個物體的特性；所以一個紅色物體被表述為有紅色的特性。性質可以被當作物體只憑自身的一種構成（form），它可以擁有其他性質。性質被認為有別於擁有它的物體。所以一階邏輯不能表達下列陳述，"對於所有的性質 P，..." 或"存在著性質 P，..."。
但是，一階邏輯足夠強大了，它可以形式化全部的集合論和幾乎所有的數學。把量化限制於個體（individual）使它難於用於拓撲學目的，但它是在數學底層經典的邏輯理論。它是比句子邏輯強比二階邏輯弱的理論。
一階邏輯的定義
謂詞演算構成如下
生成規則（就是形成合式公式的遞歸定義）。
變換規則（就是推導定理的推理規則）。
公理或公理模式的（可能的可數的無限）集合。
有兩種類型的公理： 邏輯公理，它是對於謂詞演算有效的，和非邏輯公理，它是在特殊情況下為真的，就是說，在它所在的理論的標準解釋中是真的。例如，非邏輯的皮亞諾公理在算術的符號主義標準解釋下是真的，但是對於謂詞演算它們不是有效的。
在公理的集合是無限的的時候，需要能判定給定的合式公式是否是一個公理的一個算法。進一步的，應當有可以判定一個推理規則的套用是否正確的算法。
辭彙表
"辭彙表"構成如下
大寫字母 P,Q,R,... 是謂詞變數。
小寫字母 a,b,c,... 是（個別的）常量。
小寫字母 x,y,z,... 是（個別的）變數。
小寫字母 f,g,h,... 是函式變數。
一階邏輯表示邏輯運算元的符號： ┐ （邏輯非），∧ （邏輯與），∨（邏輯或），→ （邏輯條件） 和（邏輯雙條件）。
表示量詞的符號：（全稱量詞），（存在量詞）。
左右圓括弧。
一些符號可以被簡略為原語（primitive）並被採納為簡寫；比如 (PQ) 是 (P → Q) ∧（Q → P) 的簡寫。運算元和量詞的最小數目是三個（如果我們定義了運算元或非或者與非則是兩個）；例如，┐，∨ 和 ㄢ足夠了。項是一個常量、變數或 n≥0 個參數的函式符號。
生成規則
合成公式
合式公式（wff）的集合按如下規則遞歸的定義：
一階邏輯書籍簡單和複雜的謂詞 如果 P 是 n 元（n ≥ 0）謂詞，則 Pa_1,...,a_n
是合式的。如果 n ≤ 1，則 P 是原子。
歸納條款 I: 如果 Φ 是 wff，則 ┐ Φ 是 wff。
歸納條款 Ⅱ： 如果 Φ 和 ψ 是 wff，則 Φ∧ ψ， Φ∨ ψ，（Φ → ψ）和（Φψ） 是 wff。
歸納條款 Ⅲ： 如果 φ 是 包含變數 x 的一個自由實例的 wff，則 砢，φ和x，φ 是 wff。（此後在x，φ 和x，φ 中x 的任何實例都被稱為約束的 — 而不是自由的。）
閉包條款： 其他東西都不是 wff。
變換（推理）規則
肯定前件充當推理的唯一規則。如果沒有公理模式，則還需要一個一致代換規則。
演算
謂詞演算是命題演算的擴展。如果命題演算被定義為十一個公理和一個推理規則（肯定前件），不計算針對邏輯等價運算元的額外定律在內，則謂詞演算可以被定義為在其上添加四個補充的公理和一個補充的推理規則。
公理擴展
下列四個公理是謂詞演算的特徵：
PRED-1:x Z(x) → Z(y)
PRED-2:Z(y) →x Z(x)
PRED-3:x (W → Z(x)) → (W →x Z(x))
PRED-4:x (Z(x) → W) → (x Z(x) → W)
它們實際上是公理模式，因為其中的謂詞字母 W 和 Z 可以被任何謂詞字母所替代，而不改變這些公式的有效性。
推理規則
叫做全稱普遍化的推理規則是謂詞演算的特徵。它可以陳述為
|- Z(x),x Z(x)
這裡的 Z(x) 假定表示謂詞演算的一個已證明的定理，而 砢娀（x) 是它針對於變數 x 的閉包。謂詞字母 Z 可以被任何謂詞字母所替代。
注意：全稱普遍化類似於模態邏輯的必然性規則，它是
- P,- □ P
元邏輯定理
在公告板中列出了一些重要的元邏輯定理。
不像命題演算，一階邏輯是不可判定性的。對於任意的公式 P，可以證實沒有判定過程，判定 P 是否有效，（參見停機問題）。（結論獨立的來自於邱奇和圖靈。）
有效性的判定問題是半可判定的。按哥德爾不完備定理所展示的，對於任何有效的公式 P,P 是可證明的。
單體謂詞邏輯（就是說，謂詞只有一個參數的謂詞邏輯）是可判定的。
詳細內容
一階邏輯在一階邏輯中描述一個數學理論，首先會涉及這個理論所討論的對象、定義在這些對象上的函式、
以及這些對象之間的關係或性質。數學理論所討論的對象稱為個體，由個體組成的非空集合稱為論域或個體域。按通常數學中的定義，一個n元函式就是從論域A的個體的所有n元組的集合至A中的一個映射。A中個體的n元組（α1，α2，…，αn）經映射F對應到A中的個體表示為F（α1，α2，…，αn）。函式增加了個體的表達形式。人們也考慮論域A中哪些n元組滿足關係R，即A中哪些n元組（α1，α2，…，αn）使得R（α1，α2，…，αn）為真。此時的R（α1，α2，…，αn）就是一個命題。
在各種關係中，相等關係是經常要用的。因為常常需要知道不同個體的表達式是否指稱同一個對象。例如3+3與2×3是否表示同一個數。
一階邏輯可以將關係或命題用命題連線詞來構成更複雜的關係或命題。當描述一些個數為無窮的對象的性質時，就需要引進量詞。例如說“對任何一個自然數，都有一個比它大的素數”時，就引進了量詞“所有個體”及“存在個體”，並且將關係或命題經量詞構成了更複雜的關係或命題。“論域中的所有個體
”稱為全稱量詞，由它所構成的命題“論域中所有的個體有某性質”，當論域中所有個體都有此性質時，此命題是真的，否則為假。“論域中存在個體”稱為存在量詞，由它所構成的命題“論域中存在個體有某性質”，當論域中某些個體有此性質時為真，否則為假。
“所有個體”、“存在個體”中，量詞加在論域的個體上，稱為一階量詞。在一階邏輯中使用的量詞僅限於一階量詞。“所有函式”、“存在函式”、“所有關係”和“存在關係”是二階量詞。此外還有更高階的量詞。相應地也有二階邏輯、高階邏輯等。
一階邏輯書籍按照建立形式系統的一般原則（見邏輯演算），一階邏輯的形式系統應包括它的語言，即一階語言，以及邏輯公理和推理規則。
一階語言的符號包括以下幾類。
① 個體變元x，y，z，…。
② 函式符號（表示函式），g，h，…；個體符號（表示論域中的個體） α，b，с，…；及謂詞（表示關係）p,Q，R，…。其中有一個二元謂詞=，稱為等詞（表示恆同關係）。
③ 命題聯結詞┐，∧，∨，→，以及量詞（存在量詞），（全稱量詞）。
①，③及等詞稱為邏輯符號，其他符號，即等詞外的②稱為非邏輯符號。
歸納地定義一階語言的項和公式，也稱之為形成規則。項的定義：
① 變元和個體符號是項。
② 若t1,t2，…，tn是項，是一個n元函式符號，則（t1,t2，…，tn）是項。
公式可定義為：
① 若t1,t2，…，tn是項，p是n元謂詞符號，則p(t1,t2，…，tn）是公式，也稱為原子公式。
② 若A是公式，則塡A是公式；若A，B是公式，則A∧B，A∨B，A→B，A凮B是公式。
③ 若A是公式，則xA，凬xA是公式。
如果變元x出現在公式 A中形如xB或凬xB的部分，稱這個出現為x在A中的約束出現；否則，稱為x在A中的自由出現。例如在公式x=0∨x(x>0）中，第一個x是自由出現，第二、三個x是約束出現。沒有變元自由出現的公式稱為閉公式。
謂詞演算作為一個形式系統，可以規定它的解釋。給定一個論域，對於謂詞演算中出現的個體符號、函式符號及謂詞依次解釋為論域中的個體及定義在此論域上的函式及關係。此論域及其對於謂詞演算中形式符號的解釋稱為該演算的一個結構或模型。由對於個體符號和函式符號的解釋可知，項可解釋為複合函式，它指稱個體。原子公式p(t1,t2，…，tn）解釋為t1,t2，…，tn所指稱的個體滿足n元關係p。若公式A(x）表示關係，則凬xA(x）解釋為論域中所有個體滿足關係A，xA(x）解釋為論域中存在某個體滿足關係A。
謂詞演算的推理規則可規定如下：
謂詞演算的邏輯公理陳述邏輯符號的性質，分為三類：
一階邏輯書籍① 命題公理 將重言式（見命題邏輯）中出現的命題變元代之以謂詞演算中的任意公式後得
到的公式；
② 恆同公理 x=x及相等性公理
③ 替換公理 Ax【α】→xA及凬xA→Ax【α】，其中Ax【α】表示將公式A中所有x的自由出現代之以項α。
謂詞演算的公理，即邏輯公理並不界定具體的函式或關係，而僅僅處理邏輯詞項的一般性質。換言之，對它的個體符號、函式符號、及謂詞的解釋可以是任意論域中的任意個體、函式及關係。謂詞演算的這個抽象性質對於近年來模型論的發展是本質的。
在謂詞演算的框架中，用形式語言表述數學的公理（並不一定能完全表述），就得到不同數學理論的形式系統。這類形式公理刻畫了某些具體的非邏輯符號的性質，稱為非邏輯公理。例如：
全序理論的形式系統中僅有一個非邏輯符號二元謂詞≤。除邏輯公理外，它還有非邏輯公理：①x≤y∧y≤z→x≤z;②x≤y∧y≤x→x=y；③x≤x；④x≤y∨y≤x。自然數集合及其上的順序關係就是全序理論的一個模型。
群論的形式系統中只有兩個非邏輯符號：個體符號1及二元函式符號·。它的非邏輯公理為：① x·（y·z)=(x·y）·z；②x·1=x；1·x=x；③y(x·y=1∧y·x=1）。任何一個群都是它的模型。
一階邏輯書籍數論的形式系統中的非邏輯符號有：個體符號0，一元函式符號s及兩個二元函式符號+及·。數論（或皮亞諾算術）的公理為：①塡s(x)=0，②s(x)=s(y）→x =y，③x+0=x，④ x+s(x)=s(x+y），⑤ x·0=0，⑥x·s(y)=（x·y）+x，⑦若A為系統內的公式，x0在A中自由出現，則對每個這樣的公式A，有公理自然數的算術
就是它的一個模型。
陳述在一階語言中，由邏輯公理、非邏輯公理及推理規則推出的全部形式定理（見邏輯演算）稱為一階理論，記為T。為區別不同的一階理論T，只要指出T的語言中的非邏輯符號及非邏輯公理就夠了。任何一階理論都包含了謂詞演算作為它的子系統。
在謂詞演算的任意模型中均為真的公式稱為永真的或有效的公式。例如，公式A(x,y）∨塡A(x,y）就是有效的公式，而x≤y∨y≤x就不是有效的。因為在全序結構中，對x，y在個體域中的任意取值，該公式的解釋均為真。而在半序結構中，例如該結構的論域為一個集合的全體子集的集合，≤解釋為集合的包含關係，那么上式的解釋當x，y取任意的兩個子集時就不都是真的了。
一階邏輯書籍直觀上看，邏輯的定理應當是在一切可能的世界中均為真的定理。在一定意義下，謂詞演算滿足這個性質。可以驗證，謂詞演算的公理均為有效的，它的推理規則的假設有效則結論也必有效。因此，謂詞演算的所有定理都是有效的。這個性質稱為謂詞演算的有效性或可靠性。反之，任意有效的公式必為謂詞演算的定理。這就是著名的哥德爾完備性定理。由K.哥德爾於1930年證明。
用├A表示A是謂詞演算的形式定理，即A 是系統內的定理。而可靠性與完備性刻畫了整個形式系統的性質，是關於系統的定理，也稱為元定理。形式系統的性質是數理邏輯主要的研究對象之一。
由謂詞演算的有效性及完備性容易推知一階理論的可靠性與完備性。使一階理論 T的所有公理為真的結構稱為T 的一個模型。若T的一個公式A在T 的任意模型中均有效，稱A在T中有效，記為T喺A。A是T的定理記為T├A。那么T的可靠性與完備性就可以陳述為T├ A的充分必要條件為T 喺A。
若不存在A使得T├A且├塡 A，則稱T是協調的。
若T 是協調的，則T 必有模型（廣義完備性定理）。
形如x1，x2，…，xnB 的公式稱為前束型公式，其中xi表示 xj或凬xj，B 是一個不含量詞的公式。任何一個一階理論T（當T 的非邏輯公理集為空集時就是一個謂詞演算）的公式A，都有一個公式A′，使得T├A凮A┡，其中A┡為前束型公式x1,x2，…，xηB，且B中的非邏輯符號均在A中出現。A′也稱為A的前束範式。此性質可用於對謂詞演算或一階理論的公式進行分類上。此時只需考慮前束範式中的量詞，將它作為公式複雜性的一種測度。
