概述
形式邏輯的最根本部分，也是最基本的邏輯系統或理論。在謂詞邏輯中，除研究 複合命題的命題形式、命題聯結詞的邏輯性質和規律外，還把命題分析成個體詞、謂詞和量詞等非命題成分，研究由這些非命題成分組成的命題形式的邏輯性質和規律。謂詞邏輯把 命題邏輯作為子系統，但為了研究方便，同時也由於它具有某些重要的特殊性質，命題邏輯通常又作為一個獨立的系統先研究，而在謂詞邏輯部分則集中研究由非命題成分組成的命題形式和量詞的邏輯性質與規律。只包含個體謂詞和個體量詞的謂詞邏輯稱為一階謂詞邏輯，簡稱 一階邏輯，又稱狹義謂詞邏輯。此外，還包含高階量詞和高階謂詞的稱為 高階邏輯。謂詞邏輯也分為經典的謂詞邏輯和非經典的謂詞邏輯，後者包括作為子系統的非經典的 命題邏輯。經典的一階謂詞邏輯是謂詞邏輯的基本部分。第一個完整的謂詞邏輯系統是G.弗雷格在1879年建立的。K.哥德爾等人系統地研究了謂詞邏輯的元邏輯問題，證明了重要的 定理。
注意事項
在謂詞邏輯中，使用量詞應注意以下幾點：
(1) 在不同個體域中， 命題符號化的形式可能不同，命題的真值也可能會改變.
(2) 在考慮 命題符號化時，如果對個體域未作說明，一律使用全總個體域.
(3) 多個量詞出現時，不能隨意顛倒它們的順序，否則可能會改變命題的含義.
謂詞公式只是一個符號串，沒有什麼意義，但我們給這個符號串一個解釋，使它具有真值，就變成一個命題. 所謂解釋就是使公式中的每一個變項都有個體域中的元素相對應.
在謂詞邏輯中， 命題符號化必須明確個體域，無特別說明認為是全總個體域。一般地，使用全稱量詞"，特性謂詞後用®；使用存在量詞$，特性謂詞後用Ù.
公式與解釋
謂詞公式
h謂詞公式，由原子公式、聯結詞和量詞可構成謂詞公式(嚴格定義見教材). 命題的符號化結果都是謂詞公式.
例如"x(F(x)®G(x))，$x(F(x)ÙG(x))，"x"y(F(x)ÙF(y)ÙL(x,y)®H(x,y))等都是 謂詞公式.
h變元與轄域，在謂詞公式"xA和$xA中，x是指導變元，A是相應量詞的轄域. 在"x和$x的轄域A中，x的所有出現都是約束出現，即x是約束變元，不是約束出現的變元，就是自由變元. 也就是說，量詞後面的式子是轄域. 量詞只對轄域內的同一變元有效.
h換名規則，就是把 公式中量詞的指導變元及其轄域中的該變元換成該公式中沒有出現的個體變元，公式的其餘部分不變.
h代入規則，就是把公式中的某一自由變元，用該公式中沒有出現的個體變元符號替代，且要把該公式中所有的該自由變元都換成新引入的這個符號.
解釋(賦值)
h解釋(賦值)，謂詞公式A的個體域D是非空集合，則
(1) 每一個常項指定D中一個元素；
(2) 每一個n元函式指定Dn到D的一個函式；
(3) 每一個 n元謂詞指定Dn到{0,1}的一個謂詞；
按這個規則做的一組指派，稱為A的一個解釋或 賦值.
在有限個體域下，消除量詞的規則為：如D={a1,a2,…,an}，則
h謂詞公式分類，在任何解釋下，謂詞公式A取真值1，公式A為邏輯有效式(永真式)；在任何解釋下謂詞公式A取真值0，公式A為永假式；至少有一個解釋使公式A取真值1，公式A稱為可滿足式.
命題形式
最簡單的命題，即所謂原子命題，都可以分析為個體詞和謂詞兩類成分。例如,在“5是素數”、“7大於3”這兩個命題中，5、7和 3是個體詞，“是素數”、“大於”是謂詞。在邏輯中，一個論域中的元素稱為個體，個體詞是表示個體的符號；表示某個論域中的一個特定個體的符號稱為個體常項或個體常元，個體常項也就是它所表示或指稱的那個個體的名字；不表示某一確定論域中的特定個體的個體詞，稱為個體變項或個體變元，用符號 , , 和 1, 1, 1,…表示；個體變項取任一論域中的任一個體為值。謂詞是表示個體的性質和個體之間關係的符號。個體的性質也稱一元關係，表示個體的性質即一元關係的稱為一元謂詞。兩個個體之間的關係稱為二元關係，n個個體之間的關係稱為n元關係。表示二元關係的為二元謂詞，表示 n元關係的為 n元謂詞。如“是素數”就是一元謂詞，“大於”是二元謂詞,“在…之間”是三元謂詞。表示某一論域中的特定的性質或關係的稱為謂詞常項或謂詞常元,“是素數”等都是謂詞常項。不表示某一確定論域中的特定性質或關係的稱為謂詞變項或謂詞變元。謂詞變項用符號 , , 和 1， 1， 1，…表示。謂詞變項也分為一元的、二元的、…,n元的，等等。謂詞變項的元數可以明晰地標示出來，如 1表示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,…;F 2,G 2,H 2,…；等等。不過,省去上標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也是語法變元，屬於元語言。
量詞轄域
量詞的轄域指一量詞後的最短 公式，表示一個量詞在一個公式中的 作用範圍。例如,在公式 (∨ )【(凬 ) ( )→ ( )】中，(凬 )的轄域是公式 ( )，(凬 )的轄域是公式【(凬 ) ( )→ ( )】。 變元α在一個公式A中的某次出現是約束出現，如果α的這次出現是在(凬α)中或（凬α）的轄域中；α在一公式 A中的某次出現是自由出現，如果α在A中的這次出現不是約束的。例如，在公式(凬 )【(凬( ) ( )→ ( )】中, 和 的兩次出現都是約束的；在公式【(凬 ) ( )→ ( )】中, 的兩次出現是約束的, 的唯一一次出現是自由的。個體變元α可以在A中既有約束出現又有自由出現, 例如, (凬α) ( )→ ( )。如果個體變元α在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(α)中的每處自由出現而得的公式。
根據④以下的公式都是 公理：
(凬 )【 ( )→ ( , )】→【 ( )→(凬 )G( , );
(凬 )【(凬 ) ( )→ ( )】→【(凬 ) ( )
→(凬 ) ( )】。
但公式(凬 )【 ( )→ ( , )】→【 ( )→(凬 ) ( , )】卻不是 公理，因為它不符合圖式④中關於 在 ( )中沒有自由出現的規定。
根據圖式⑤，以下的公式都是公理：
(凬 ) ( )→ ( );
(凬 ) ( )→ ( );
(凬 ) ( , )→ ( , );
(凬 )【 ( )→ ( , )】→【 ( )→(凬 ) ( , )】。
但 (凬 ) 【 ( )→(凬 ) ( , )】→【 ( )→(凬 ) ( , )】不是 公理。因為該公式的 對 ( )→(凬 ) ( , )中的 不是自由的，不符合圖式⑤的條件。
變形規則也稱推理規則。變形規則的陳述，除使用語法變元，還使用語法符號儱。符號儱在一個公式的前面，表示緊接在儱後面的公式是 定理。例如，儱A,表示A是定理。 F的變形規則有兩條，即：①分離規則,從A和A→B，可以推出B；②概括規則,從A,可以推出(凬α)A。
F中的一個證明，指一有窮 公式序列A1,A2, …, An，其中的每一Ak(k=1,2,…,n)或者是一個 公理，或者是由公式Ai和 Aj(i,jj=Ai→Ak)套用分離規則而得，或者是由公式Aj(jk=(凬α)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、jj=Ci→Ck)套用分離規則而得,或者是由Cj(jn是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。
