= 一阶谓词逻辑 =

'''一阶逻辑'''（First-order logic）是数学家、哲学家、语言学家使用的一种形式[[演绎]]系统。它有很多名字包括：一阶谓词演算、低等谓词演算、一阶逻辑的语言或谓词逻辑。不像[[自然语言]]如[[英语]]，FOL 使用由数学结构来解释的完全无歧义的[[形式语言]]。一阶逻辑是通过允许在给定[[论域]]的[[个体]]上的量化而扩展[[命题逻辑]]的演绎系统。例如，在 FOL 中可陈述“所有个体都有性质 P”。

命题逻辑处理简单的陈述性[[命题]]，一阶逻辑补充覆盖了[[谓词]]和[[量词]]。例如下列句子：“[[苏格拉底]]是男人”，“[[柏拉图]]是男人”。在命题逻辑中，它们是两个无关的命题，比如指示为 p 和 q。但是在一阶逻辑中，这两个句子将由同一个性质联系起来：Man(x)，这里的 Man(x) 意味着 x 是个男人。在 x = 苏格拉底时我们得到了第一个命题 p，而在 x = 柏拉图时我们得到了第二个命题 q。这种构造在介入了[[量词]]的时候允许更加强力的[[逻辑]]，比如“对于所有 x...”。例如，“对于所有 x，如果 Man(x) 则...”。没有量词的话，所有在 FOL 中的有效论证在命题逻辑中也有效的，反之亦然。

一阶理论构成自[[公理]]的[[集合]]（通常[[有限]]的或[[递归]]可[[枚举]]的）和给定底层可演绎性关系从它们可演绎出的那些陈述。“一阶理论”通常意味着某个公理集合和“与之在一起的[[完备]]（和可靠）的一阶逻辑公理化”，它闭合在 FOL 的规则之下。（对任何这种系统 FOL 将引出同样的抽象可演绎性关系，所以我们在头脑中不需要有固定的公理化系统。）一阶语言有足够的表达能力来形式化两个重要的数学理论：ZFC [[集合论]]和[[皮亚诺算术]]。但是一阶语言不能无条件的表达[[可数性]]的概念，即使它在一阶理论 ZFC 中在 ZFC 符号论的预期释义下是可表达的。这种想法可以用二阶逻辑无条件的表达。

== 词汇表 ==
----
 * [[谓词]]（或[[关系]]）的集合，经常指示为大写字母 P, Q, R, ... 。 
 * [[常量]]的集合，经常指示为小写字母，开始于字母 a, b, c, ...。 
 * [[函数]]的集合，经常指示为小写字母 f, g, h, ... 。 
 * [[变量]]的有限集合，经常指示小写字母，结束于字母 x, y, z, ...。 
 * 表示[[逻辑算子]]（或[[连结词]]）的符号：（[[逻辑非]]）~（或┐）, （[[逻辑与]]、[[合取]]）∧, （[[逻辑或]]、[[析取]]）∨，（[[逻辑条件]]）→，（[[逻辑双条件]]）↔。 
 * 表示量词的符号：（[[全称量词]]∀）, （[[存在量词]]∃）. 


参见: [[命题逻辑]] [[离散数学]] [[人工智能]]