形式邏輯的最根本部分，也是最基本的邏輯系統或理論。在謂詞邏輯中，除研究複合命題的命題形式、命題聯結詞的邏輯性質和規律外，還把命題分析成個體詞、謂詞和量詞等非命題成分，研究由這些非命題成分組成的命題形式的邏輯性質和規律。謂詞邏輯把命題邏輯作為子系統，但為瞭研究方便，同時也由於它具有某些重要的特殊性質，命題邏輯通常又作為一個獨立的系統先研究，而在謂詞邏輯部分則集中研究由非命題成分組成的命題形式和量詞的邏輯性質與規律。隻包含個體謂詞和個體量詞的謂詞邏輯稱為一階謂謂詞邏輯，簡稱一階邏輯，又稱狹義謂詞邏輯。此外，還包含高階量詞和高階謂詞的稱為高階邏輯。謂詞邏輯也分為經典的謂詞邏輯和非經典的謂詞邏輯，後者包括作為子系統的非經典的命題邏輯。經典的一階謂詞邏輯是謂詞邏輯的基本部分。第一個完整的謂詞邏輯系統是G.弗雷格在1879年建立的。K.哥德爾等人系統地研究瞭謂詞邏輯的元邏輯問題，證明瞭重要的定理。
命題形式 最簡單的命題，即所謂原子命題，都可以分析為個體詞和謂詞兩類成分。例如，在“5是素數”、“7大於3”這兩個命題中，5、7和3是個體詞，“是素數”、“大於”是謂詞。在邏輯中，一個論域中的元素稱為個體，個體詞是表示個體的符號；表示某個論域中的一個特定個體的符號稱為個體常項或個體常元，個體常項也就是它所表示或指稱的那個個體的名字；不表示某一確定論域中的特定個體的個體詞，稱為個體變項或個體變元，用符號x，y，z和x1，y1，z1，…表示；個體變項取任一論域中的任一個體為值。謂詞是表示個體的性質和個體之間關系的符號。個體的性質也稱一元關系，表示個體的性質即一元關系的稱為一元謂詞。兩個個體之間的關系稱為二元關系，n個個體之間的關系稱為n元關系。表示二元關系的為二元謂詞，表示 n元關系的為 n元謂詞。如“是素數”就是一元謂詞，“大於”是二元謂詞，“在…之間”是三元謂詞。表示某一論域中的特定的性質或關系的稱為謂詞常項或謂詞常元，“是素數”等都是謂詞常項。不表示某一確定論域中的特定性質或關系的稱為謂詞變項或謂詞變元。謂詞變項用符號F，G，H和F1，G1，H1，…表示。謂詞變項也分為一元的、二元的、…，n元的，等等。謂詞變項的元數可以明晰地標示出來，如F1表示F是一元的，G2表示G是二元的，但也可以不這樣做。在一公式中，一個謂詞變項後面跟的個體變項的個數，就表示這個謂詞變項的元數。例如，F(x)中F是一元的，G(x，y)中G是二元的，H(x1，x2，…，xn)中H是n元的。同一個符號，比如F，在不同的公式中可以表示不同元數，但在一個復雜的公式中，同一符號的幾處出現是同一個謂詞變項。應用個體變項和謂詞變項，“5是素數”、“7大於3”這兩個原子命題的形式可分別表示為F(x)和G(x，y)這兩個公式。一般地陳述n個個體間有某關系的原子命題的形式，用一個 n元謂詞變項後面跟n個個體變項的公式表示，該公式為:F(x1，x2，…，xn)。表示原子命題的形式的公式稱為原子公式。
除瞭個體詞和謂詞，組成命題的成分還有量詞。量詞是命題中表示數量的詞，它分為全稱量詞和存在量詞。例如，在“所有闊葉植物是落葉植物”、“有的水生動物是肺呼吸的”這兩個命題中的“所有”、“有的”都是量詞，其中前者是全稱量詞，後者為存在量詞。在漢語中，“所有”、“一切”、“凡”等表示全稱量詞，“有的”、“有”、“至少有一”等表示存在量詞。全稱量詞是在符號∀後跟一個個體變項(比如x)，表示為(∀x)，讀作：“對任一x”，“所有x”。存在量詞在符號ヨ後跟一個個體變項（比如x），表示為(ヨx)，讀作：“有一x”，“存在一x”。在一個公式前面加上量詞，稱為量化式，如(∀x)F(x)和(ヨx)F(x)，就分別稱為全稱量化式和存在量化式。(∀x)F(x)表示“所有x，x是F，即一切事物都是F”；(ヨx)F(x)表示“有一x，x是F，即有一事物是F”。
從原子公式出發，應用量詞和命題聯結詞¬、∧、∨、→和↔就可以構造出表示各種復雜的命題形式的公式。例如，“所有闊葉植物是落葉植物”這一命題形式的公式為：
(∀x)(F(x)→G(x))；
“有的水生動物是肺呼吸的”這一命題形式的公式為：
(ヨx)(F(x)∧G(x))。
“一切自然數有大於它的自然數”、“每人都有一個父親”這類命題，具有更復雜的公式，即：
(∀x)(F(x)→(ヨy)(F(y)∧G(x，y)))
謂詞邏輯中的這種命題形式比命題邏輯更為復雜，其數量也非常多，相應的公式的數目是無窮的。
公式的解釋 謂詞邏輯的公式可以分為普遍有效的、可滿足的和不可滿足的三類。普遍有效的公式表達謂詞邏輯的規律。為瞭刻劃公式的普遍有效性和可滿足性，首先需要說明對公式的解釋。一個解釋由一個非空個體域D和一個賦值υ組成，對每一個體變元x，υ都賦與D中的一個個體為值，如果對個體變元x1，x2，…，xn，υ分別賦以D中的個體a1，a2，…，an為值，υ對個體變元的n元組（x1，x2，…，xn）所賦之值即為(a1，a2，…，an)；對n元謂詞變元F，υ賦與F的值是D中的一個n元關系。令A為一個原子公式F(x1，x2，…，xn)，υ(A)即υ[F(x1，x2，…，xn)]的值可以為1(即真)，也可以為0（即假）。如果(x1，x2，…，xn)所賦之值(a1，…，an)屬於F所賦之值，υ(A)的值為1，否則為0。υ(A)的值為1，也就是公式A在此解釋下是D中的真命題。每一賦值 υ也給出一個真值賦值。令A、B是任意的公式。υ(¬A)的值為1，當且僅當υ(A)的值為0。υ(A∧B)的值為1，當且僅當υ(A)和υ(B)的值都為1。υ(A∨B)的值為1，當且僅當υ(A)或υ(B)的值為1。υ(A→B)的值為1，當且僅當υ(A)的值為0或υ(B)的值為1。υ(A↔B)的值為1，當且僅當υ(A)和υ(B)的值相同。υ(∀x)A(x)的值為1，當且僅當，設A的賦值已經給定，對每一D中的個體a，A(a)的值為1，即(∀x)A(x)是真的，當且僅當，設A的賦值已給定，對於D中的每一個體a，A(a)真。υ(ヨx)A(x)的值為1，當且僅當，設A的賦值已給定，有 D中的個體a，使得A(a)的值為1。
一個公式 A稱為可滿足的，如果有一不空的個體域D和賦值υ，在此解釋下，A為真。
一個公式 A稱為普遍有效的，如果對任一解釋，也就是對任一不空的個體域和任一賦值，A都真。A普遍有效也就是A常真，記為FA。
顯然，一個公式 A是普遍有效的，當且僅當，它的否定¬ A是不可滿足的。一個不可滿足的公式是常假的，也稱為矛盾的。
這裡所說的個體域、解釋、賦值、真假、普遍有效性和可滿足性等概念，都是語義概念。
公理系統 謂詞邏輯的普遍有效的公式為數無窮，在一定意義上它們都是邏輯規律。為瞭系統地研究這類規律，需要對它們作整體的考慮，將它們總括在一個系統之中。謂詞演算或者一階謂詞演算就是這樣的系統。謂詞演算是把謂詞邏輯公理化和形式化而建立的形式系統。按照對作為演算出發點的初始符號、公理和變形規則的不同挑選，可以建立不同的謂詞演算系統。在初始符號中有符號=的，稱為帶等詞的一階謂詞演算，等詞=是一個謂詞常元；不帶等詞的系統就稱為（一階）謂詞演算。構成一個謂詞邏輯的公理系統的基本要素有：初始符號、形成規則、公理和變形規則等。對此，可以從一個不帶等詞的系統 F得到說明。F的初始符號，包括個體變元、謂詞變元、聯結詞和量詞以及技術性符號四類。個體變元符號的小寫拉丁字母為：x，y，z，x1，y1，z1，x2，…；謂詞變元符號為大寫拉丁字母，即：F，G，H，F1，G1，…。在原則上，對每一n≥1，應分別列出n元謂詞變元，如：F1，G1，H1，…；F2，G2，H2，…；等等。不過，省去上標1，2，…，n，在實踐上不會產生混亂。聯結詞和量詞符號為：¬、→、∀；技術性符號為括弧（，）和逗號，。
形成規則規定怎樣的符號序列或符號的組合是F中的合式公式。合式公式經解釋後是有意義的。用來描述和討論F系統的語言即元語言的符號有：小寫希臘字母α，α1，…，αn，δ表示任意的個體變元；fn表示任意的n元謂詞變元；大寫拉丁字母X，Y表示任意的符號序列。這些符號稱為語法變元。F的形成規則有4條：①如果fn是一n元謂詞變元，α1，…，αn是個體變元，則fn(α1，…，αn)是一合式公式；
② 如果 X是合式公式，則¬X是合式公式。如果X、Y 是合式公式，則(X→Y)是合式公式；
③ 如果X是合式公式，α是個體變元，則(∀α)X是合式公式；
④ 隻有適合以上①～③的是合式公式。合式公式簡稱公式。用字母A，B，C表示任意的公式。A，B，C也是語法變元，屬於元語言。
量詞的轄域指一量詞後的最短公式，表示一個量詞在一個公式中的作用范圍。例如，在公式(∀y)[(∀x)F(x)→G(y)]中，(∀x)的轄域是公式F(x)，(∀y)的轄域是公式[(∀x)F(x)→G(y)]。變元α在一個公式A中的某次出現是約束出現，如果α的這次出現是在(∀α)中或（∀α）的轄域中；α在一公式 A中的某次出現是自由出現，如果α在A中的這次出現不是約束的。例如，在公式(∀y)[(∀(x)F(x)→G(y)]中，x和y的兩次出現都是約束的；在公式[(∀x)F(x)→G(y)]中，x的兩次出現是約束的，y的唯一一次出現是自由的。個體變元α可以在A中既有約束出現又有自由出現，例如，(∀α)F(x)→G(x)。如果個體變元α在A中自由或約束出現，它在A中就是自由或約束出現的。δ對A(α)中的α是自由的，如果在A(α)中α的自由出現不在(∀δ)的轄域中。
F的公理有無窮多條，並由5個公理圖式給出，每個圖式都代表無窮多條公理。公理圖式用語法變元陳述這5個公理圖式是：
① A→(B→A)；
②[A→(B→C)]→[(A→B)→(A→C)]；
③(¬A→¬B)→(C¬A→B→A)；
④(∀α)(A→B)→[A→(∀α)B]，如果α在A中沒有自由出現。
⑤(∀α)A(α)→A(δ)，如果δ對A(α)中的α是自由的。
該圖式的A(α)是一合式公式，α是在其中有自由出現的個體變元，A(δ)則是用δ代替α在A(α)中的每處自由出現而得的公式。
根據④以下的公式都是公理：
(∀x)[F(y)→G(x，y)]→[F(y)→(∀x)G(x，y)；
(∀x)[(∀x)F(x)→F(y)]→[(∀x)F(x)
→(∀y)F(y)]。
但公式(∀x)[F(x)→G(x，y)]→[F(x)→(∀x)G(x，y)]卻不是公理，因為它不符合圖式④中關於x在F(x)中沒有自由出現的規定。
根據圖式⑤，以下的公式都是公理：
(∀x)F(x)→F(y)；
(∀y)G(y)→G(y)；
(∀x)F(x，y)→F(y，y)；
(∀y)[F(y)→G(x，y)]→[F(y)→(∀y)G(y，y)]。
但(∀x)[F(x)→(∀y)G(x，y)]→[F(y)→(∀y)G(y，y)]不是公理。因為該公式的y對F(x)→(∀y)G(x，y)中的x不是自由的，不符合圖式⑤的條件。
變形規則也稱推理規則。變形規則的陳述，除使用語法變元，還使用語法符號儱。符號儱在一個公式的前面，表示緊接在儱後面的公式是定理。例如，儱A，表示A是定理。F的變形規則有兩條，即：①分離規則，從A和A→B，可以推出B；②概括規則，從A，可以推出(∀α)A。
F中的一個證明，指一有窮公式序列A1，A2，…，An，其中的每一Ak(k=1，2，…，n)或者是一個公理，或者是由公式Ai和 Aj(i，j＜K，且Aj=Ai→Ak)應用分離規則而得，或者是由公式Aj(j＜K)應用概括規則而得，即Ak=(∀α)Aj。一個證明也可以說是此證明的最後一個公式的證明。F中的一個公式 B是F的定理，如果B有一個證明，或者說，存在一個證明 A1，A2，…，An，這個證明的最後一個公式An即是 B。根據這個定義，每一公理都是定理，即單獨一個公理構成自身的一個證明。一個公式 B，如果存在它的一個證明，就說B是可證明的。一個公式是定理，當且僅當它是可證明的。一個公式B是由公式A1，A2，…，Am可推演的，記作：A1，A2，…，Am儱B。如果存在一個公式的有窮序列 C1，C2，…，Cn，其中每一 Ck(k=1，…，n)或者是一公理，或者是A1，…，Am中的一個，或者是由Ci、Cj(i、j＜K，且Cj=Ci→Ck)應用分離規則而得，或者是由Cj(j＜K)應用概括規則而得，並且Cn是B。如m=0，則儱B當且僅當B是一定理。
F的初始符號中不包括∧、∨、↔、ヨ這幾個符號，但它們可以通過定義引入，即：
(A∨B)定義為(¬A→B)；
(A∧B)定義為¬(A→¬B)；
(A↔B)定義為(A→B)∧(B→A)；
(ヨα)A定義為¬(∀α)¬A。
關於謂詞演算F，隻涉及符號、符號序列、符號序列的變換等等，完全沒有涉及符號、公式等的意義。這種不涉及符號、公式等的意義的研究，是語法的研究。定理、可證明性等概念，都是語法概念。而對符號、公式的解釋，以及關於公式和它的意義的關系等等，都屬於語義的研究。關於F的解釋稱為標準解釋或標準語義。在這個標準解釋下，F的公理圖式以及公理本身都是普遍有效的，而變形規則具有保持普遍有效性的性質，即從普遍有效的公式經應用變形規則而得到的公式也是普遍有效的。所以，F的定理都是普遍有效的。
謂詞演算F有許多元邏輯定理或稱元定理。不過元定理並不是F中的定理，而是關於F的定理，是對F這個系統的某些重要性質的研究的結果。重要的元定理有3個：①可靠性定理，表述為：如果儱A，則⊨A。這條定理表明F的定理都是普遍有效的。
② 一致性定理。這條定理表明F是一致的，即不存在一個公式A，A和¬A都是定理。
③ 完全性定理，它表述為：如果⊨A，則儱A。該定理表明，F在凡普遍有效的公式都是定理這一意義上是完全的。
可靠性定理表明，謂詞演算F對演繹推理形式的反映是可靠的。設A是一個推理的前提的命題形式，B是結論的命題形式，這個推理的形式就是 A→B。F的定理都是普遍有效的，這就意味著F隻反映有效的推理形式。而完全性定理則表明，F對有效推理的形式的反映是完全的。設A→B是一個有效的推理的形式，當A真時B一定真，A→B是普遍有效的，因而是F的定理。這兩個定理也表明，對F來說，語法和語義是一致的、相符合的。也就是說，可證明性和普遍有效性是相符合的，一個公式是可證明的或是定理，當且僅當它是普遍有效的。
自然推理系統 除瞭F這樣的形式系統，謂詞邏輯還可用另一種方式系統化，即建立自然推理系統。例如，有一個與F相應的自然推理系統，其初始符號和形成規則與F相同。在該系統的規則中，A、B是任意公式，A(α)、A(δ)也和FA1，…，An⊢A1(i=1，…，n)。這是肯定前提規則；
(τ)如果г⊢Δ⊢（Δ不空），則г⊢A。這是演繹推理傳遞規則；
(→)如果г，¬A⊢B，並且г，¬A⊢¬B，則г⊢A。這是否定詞消去規則；
(→﹣)A→ B，A⊢B。這是蘊涵詞消去規則；
(→﹢)如果г，A⊢B，則г⊢A→B。它是蘊涵詞引入規則；
(凾)(∀α)A(α)⊢A(δ)，這是全稱量詞消去規則；
(刄)如果г⊢A(α)，α在 г中的公式中沒有自由出現，則г儱(∀α)A(α )。這是全稱最詞引入規則。
規則(τ)表示，從г能推出Δ，從Δ能推出A，則從г能推出A，推出關系是傳遞的。規則(→)也稱反證律。在這一自然推理系統中，符號∨、∧、↔和ヨ也可以通過定義引入，並導出相應的規則。
關於這個自然推理系統，有如下的結果：如果 A普遍有效，即⊨A，則⊢A；並且，如果⊢A，則A普遍有效。在F和這個自然推理系統之間，有如下關系：對任一公式A，如果A在F中可證，即儱A，則⊢A；反之，如果A在自然推理中不需任何前提就能推出，即⊢A，則 A在F中可證。這個自然推理系統也和F一樣具有可靠性、一致性和完全性。
參考書目
胡世華、陸鐘萬：《數理邏輯基礎》，科學出版社，北京，1981（上冊），1982（下冊）。
莫紹揆：《數理邏輯教程》，華中工學院出版社，武漢，1983。