谓词逻辑

在数理逻辑中，谓词逻辑（英語：predicate logic）是符号形式系统的通用术语，包括一阶逻辑、二阶逻辑、多类逻辑（英语：Many-sorted logic）和无穷逻辑等。与命题逻辑不同，谓词逻辑引入了个体词（英语：Non-logical symbol）、谓词、量词和变元，能够表达命题逻辑无法处理的内部结构。

谓词逻辑是现代数理逻辑的核心，为数学基础、计算机科学和语言学的形式化提供了基础工具。一阶谓词逻辑是最广泛使用的形式系统，具有完备性、紧致性等优良性质，是公理化集合论和模型论的基础。

历史

谓词逻辑的历史可追溯至亚里士多德的三段论，但其现代形式直到19世纪末才诞生。1879年，戈特洛布·弗雷格在《概念文字》（Begriffsschrift）中首次建立了完备的谓词逻辑形式系统，引入了量词和变元，被公认为现代谓词逻辑的诞生标志。

1880年代，查尔斯·桑德斯·皮尔士独立发展了量化理论，引入了全称量词∀和存在量词∃的符号表示。1910-1913年，伯特兰·罗素和阿弗烈·诺夫·怀特海德在《数学原理》中进一步发展了谓词逻辑系统。

1928年，大卫·希尔伯特和威廉·阿克曼在《理论逻辑原理》中系统阐述了一阶谓词逻辑。1929年，库尔特·哥德尔在博士论文中证明了一阶谓词逻辑的完备性定理。1930年代，阿隆佐·邱奇和艾伦·图灵证明了谓词逻辑的不可判定性。

语法

谓词逻辑的语法定义了哪些符号串构成合法的公式。

字母表

谓词逻辑的语言包括以下符号：

个体变元：x, y, z, …
个体常元：a, b, c, …
函数符号：f, g, h, …（每个带有指定的元数）
谓词符号：P, Q, R, …（每个带有指定的元数）
逻辑连接词：¬, ∧, ∨, →, ↔
量词：∀（全称量词）、∃（存在量词）
等词：≈（可选）

项与公式

项（term）是个体常元、变元和函数应用：若t₁,…,tₙ是项，f是n元函数符号，则f(t₁,…,tₙ)也是项。

公式（formula）递归定义如下：

若P是n元谓词符号，t₁,…,tₙ是项，则P(t₁,…,tₙ)是原子公式
若φ和ψ是公式，则¬φ、φ∧ψ、φ∨ψ、φ→ψ、φ↔ψ是公式
若φ是公式，x是变元，则∀xφ和∃xφ是公式

自由变元与约束变元

在公式∀xφ或∃xφ中，φ称为量词的辖域，x在辖域中的出现称为约束出现。不在任何量词辖域中的变元称为自由变元。不含自由变元的公式称为句子。

语义

谓词逻辑的语义通过模型（结构）来定义。

模型

一个模型M由以下要素构成：

论域（domain）：一个非空集合D
解释（interpretation）：为每个常元指定D中的元素，为每个函数符号指定D上的函数，为每个谓词符号指定D上的关系

真值条件

公式在模型M和变元赋值s下的真值递归定义。关键条款包括：

M ⊨ P(t₁,…,tₙ)[s]当且仅当（‖t₁‖,…,‖tₙ‖）在P的解释中
M ⊨ ∀xφ[s]当且仅当对每个d ∈ D，M ⊨ φ[s(x/d)]
M ⊨ ∃xφ[s]当且仅当存在d ∈ D使得M ⊨ φ[s(x/d)]

一个公式φ是有效的（valid），若它在所有模型中为真；φ是可满足的（satisfiable），若存在某个模型使其为真。

一阶谓词逻辑

一阶谓词逻辑（first-order logic, FOL）是应用最广泛的谓词逻辑系统，仅允许对个体变元进行量化，不允许对谓词或函数进行量化。

元定理

一阶逻辑具有以下重要性质：

可靠性定理（Soundness）：所有可证明的公式都是有效的。
哥德尔完备性定理（1929）：所有有效的一阶公式都是可证明的。
紧致性定理（Compactness）：一组一阶句子有模型，当且仅当每个有限子集有模型。
勒文海姆-斯科伦定理：若一阶理论有无限模型，则存在任意基数的模型。
不可判定性（邱奇-图灵定理）：一阶逻辑的有效性问题是递归不可判定的。

局限性

一阶逻辑虽然强大，但存在局限性：无法表达「有限性」、「可数性」等概念，也无法对数学归纳法进行完全形式化。这些局限性促使了高阶逻辑的发展。

高阶谓词逻辑

二阶逻辑允许对谓词和函数进行量化，表达力强于一阶逻辑，但失去了完备性和紧致性等良好性质。高阶逻辑（如简单类型论）进一步发展了这些思想，在类型论和数学基础中具有重要地位。

其他变体

多类逻辑（英语：Many-sorted logic）（Many-sorted logic）：论域分为多个不相交的类，每个量词指定量化的类。
无穷逻辑（Infinitary logic）：允许无限长的公式和无限长的合取/析取。
直觉主义谓词逻辑：基于直觉主义逻辑的谓词逻辑，拒绝排中律。
模糊谓词逻辑：真值可取区间[0,1]中的值的谓词逻辑。

应用

谓词逻辑在多个领域有重要应用：

数学：公理化集合论（ZFC）、皮亚诺算术、模型论均建立在一阶逻辑之上。
计算机科学：逻辑编程（Prolog）、数据库查询语言（SQL）、形式化验证、自动定理证明。
语言学：蒙太格语法利用高阶谓词逻辑来刻画自然语言的语义。广义量词理论研究自然语言中量词的逻辑性质。

参见

命题逻辑
一阶逻辑
二阶逻辑
数理逻辑
形式系统

Classical Logic. Stanford Encyclopedia of Philosophy. [2026-05-13].
Hamilton, A. G. Logic for Mathematicians. Cambridge University Press. 1978. ISBN 0-521-21838-1.
Frege, G. Begriffsschrift. Louis Nebert. 1879.
Peirce, C. S. On the Algebra of Logic. American Journal of Mathematics. 1885, 7: 180–202.
Whitehead, A. N.; Russell, B. Principia Mathematica. Cambridge University Press. 1910–1913.
Gödel, K. Über die Vollständigkeit des Logikkalküls. Doctoral dissertation. 1929.
Enderton, H. B. A Mathematical Introduction to Logic 2nd. Academic Press. 2001. ISBN 978-0-122-38452-3.

[sep-classical-1] Classical Logic. Stanford Encyclopedia of Philosophy. [2026-05-13].

[hamilton-2] Hamilton, A. G. Logic for Mathematicians. Cambridge University Press. 1978. ISBN 0-521-21838-1.

[frege-3] Frege, G. Begriffsschrift. Louis Nebert. 1879.

[4] Peirce, C. S. On the Algebra of Logic. American Journal of Mathematics. 1885, 7: 180–202.

[pm-5] Whitehead, A. N.; Russell, B. Principia Mathematica. Cambridge University Press. 1910–1913.

[godel-complete-6] Gödel, K. Über die Vollständigkeit des Logikkalküls. Doctoral dissertation. 1929.

[enderton-7] Enderton, H. B. A Mathematical Introduction to Logic 2nd. Academic Press. 2001. ISBN 978-0-122-38452-3.