数理逻辑最基本的形式系统。又称一阶逻辑。一个可以回答真假的命题，不仅可以分析到简单命题，还可以分析到其中的个体、量词和谓词。个体表示某一个物体或元素，量词表示数量，谓词表示个体的一种属性 。例如用P(x)表示x是一棵树，则P(y)表示y是一棵树，用Q(x)表示x有叶 ，则Q(y)表示y也有叶。这里P、Q是一元谓词，x，y是个体，公式"x(P(x)→Q(x))表示每一棵树都有叶子 ，这里"是全称量词表示“每一个” 。公式$x(P(x)∧Q(x))表示有一棵没有叶的树，这里$是存在量词，表示“存在一个”。

基本介绍

推演规则

形成规则

推理规则

举例论证

词汇表

公理(逻辑公理 量词公理 等式公理)

一阶逻辑的元逻辑定理

基本介绍

谓词演算

predicate calculus

除了一元谓词 ，也可以有二元 ，三元 ，甚至多元谓词。事实上，数学中的关系，函数都可以看成谓词。例如x≤y可以看成二元谓词，x+y=z可以看成三元谓词，因此谓词演算的公式可表示数学中的一些命题。例如若用 Q(x）表示x是有理数，则公式(*)"x"y(Q(x）∧Q(y)∧x≤y→$z(Q(z）∧x<z<y)) 表示任意两个不相等的有理数中间一定存在另一个有理数。这就是有理数的稠密性。

谓词可以在一定的个体集合中给出解释，谓词公式可以在这样的个体集合中取到真假值。例如在实数集R中解释Q(x)为x是有理数，则谓词公式（*）取值为真。如果在R中解释Q(x）为“x是整数”，谓词公式（*）就取值为假了。谓词公式在个体集合中取值的严格定义称为基本语义定义，这个定义是波兰籍数学家A.塔尔斯基在20 世纪 30年代给出的。给定了谓词解释的个体集合称为模型。基本语义定义使谓词公式和模型都可以被当作数学对象加以研究。一个谓词公式在任意一个模型中都取真值，就称之谓恒真式。两个谓词公式A，B在任意模型的任何一种解释下都取相同的值，就称A，B逻辑等价。命题演算中的恒真式和等价式所反映的规律在谓词演算中仍成立。谓词演算中还有一些有关量词的等价式，如："xP(x)&Ucirc;$鰔黀（x），"x(j→ψ）&Ucirc;j→"xψ（x不在j中自由出现），"x(j→ψ）?xj→ψ（x不在ψ中自由出现）。利用这些有关量词的等价式作等价变换，可以把任何一个谓词公式的量词移到公式的最前面，得到与之等价的前束标准形公式。形如Qx1，Qx2，… ，QxnB的公式称为前束型公式 ，其中Qxi表示$xi或"xi，B是一个不含量词的公式。

推演规则

谓词演算也研究谓词公式的推演。谓词演算自然推演的一些规则为：

①全称量词消去

②全称量词引入

③存在量词消去

④存在量词引入

这些规则中横线上是条件，横线下是结论，j(x）是含自由变元x的谓词公式，y是不在j(x）中出现的变元 ，c是特定的个体常元，j(y），j(c）是以y，c分别代替j(x）中所有自由出现的x得到的谓词公式。与命题公式的推演不同 ，谓词公式的推演要求条件是恒真式时得到的结论也是恒真式。

谓词演算也可以公理化。从符号到公式的定义，从公理到推演都严格形式化，构成完全的公理系统，使系统所推演出的都是恒真式，且每个恒真式都能从公理推演出来。与命题演算不同的是，谓词演算是一个不可判定的系统，即不存在一个算法来判定谓词公式是否恒真式。

谓词演算是命题演算的扩展，命题演算对于描述更复杂的数学结构是不充分的。从文法上说谓词演算在现存的命题演算上增加了“谓词-主词结构”和量词。主词是给定的个体群组（集合）的一个成员的名字，而谓词是在这个群组上的关系，一元谓词在哲学中称为性质，在数学中称为指示函数，在数理逻辑中称为布尔值函数。

形成规则

形成规则定义项，公式和自由变量。

项

项的集合按如下规则递归的定义：

任何常量是项。

任何变量是项。

n ≥ 1 个参数的任何表达式 f(t1,...,tn) （这里的每个参数 ti 都是项，而 f 是 n 价的函数符号） 是项。

闭包条款： 其他东西都不是项。

合式公式

合式公式（通常叫做 wff 或只是公式）按如下规则递归的定义：

简单和复杂谓词 如果 P 是 n ≥ 1 价的关系而 ai 是项，则 P(a1,...,an) 是合式的。如果等式被认为是逻辑的一部分，则 (a1 = a2） 是合式的。所有这个公式都被称为是原子。

归纳条款 I: 如果 φ 是 wff，则 &not；φ 是 wff。

归纳条款 II: 如果 φ 和 ψ 是 wff，则 （φ → ψ） 是 wff。

归纳条款 III: 如果 φ 是 wff 而 x 是变量，则x φ 是 wff。

闭包条款： 其他东西都不是 wff。

因为 &not；（φ → &not；ψ） 逻辑等价于 （φ ∧ ψ），（φ ∧ ψ） 经常用做简写。（φ ∨ ψ） 和 （φ ψ） 也是同样的道理。还有x φ 是 &not;?y &not；φ 的简写。实际中，如果 P 是 2 价关系，我们经常写 "a P b" 替代 "P a b"；例如，我们写 1 < 2 而不是 <（1 2）。类似的，如果 f 是 2 价函数，我们有时写 "a f b" 替代 "f(a b)"；例如，我们写 1 + 2 而不是 +（1 2）。经常省略某些圆括号，如果不导致歧义的话。

有时声称 "P(x) 对精确的一个 x 成立"是有用的，这可表达为！x P(x）。还可以表达为x (P(x) ∧y (P(y) → (x = y)))。

在计算机科学术语中，公式实现内置“布尔”类型，而项实现所有其他类型。

自由变量

原子公式 如果 φ 是原子公式则 x 在 φ 中是自由的，当且仅当 x 出现在 φ 中。

归纳条款 I: x 在 &not；φ 中是自由的，当且仅当 x 在 φ 中是自由的。

归纳条款 II: x 在 （φ → ψ） 中是自由的，当且仅当 x 在 φ 中是自由的或者 x 在 ψ 中是自由的。

归纳条款 III: x 在y φ 中是自由的，当且仅当 x 在 φ 中是自由的并且 x?y。

闭包条款： 如果 x 在 φ 中不是自由的，则它是约束的。

例如，在 x y (P(x) Q(x,f(x),z)) 中，x 和 y 是约束变量，而 z 是自由变量，而 w 不是二者因为它没有出现在任何公式中。

推理规则

肯定前件充当推理的唯一规则。

叫做全称普遍化的推理规则是谓词演算的特征。它可以陈述为

这里的 Z(x) 假定表示谓词演算的一个已证明的定理，而xZ(x) 是它针对于变量 x 的闭包。谓词字母 Z 可以被任何谓词字母所替代。

举例论证

有序阿贝尔群的语言有一个常量 0，一个一元函数，一个二元函数 +，和一个二元关系 ≤。所以

0,x,y 是原子项

+(x,y),+(x,+(y,(z))) 是项，通常写为 x + y,x + y z

=(+(x,y),0），≤（+(x,+(y,(z))),+(x,y)) 是原子公式，通常写为 x + y = 0,x + y - z ≤ x + y

（?xy ≤（ +(x,y),z)) ∧ (?x =(+(x,y),0)) 是公式，通常写为 (?xy x + y ≤ z) ∧ (?x x + y = 0)

代换

如果 t 是项而 φ（x) 是可能包含 x 作为自由变量的公式，则 v φ（t) 被定义为把 x 的所有自由实例替代为 t 的结果，假如在这个过程中没有 t 的自由变量变为约束的。如果某些 t 的自由变量变为了约束的，则 t 对 x 的替代首先必须把 φ 中的约束变量的名字改变为不同于 t 的自由变量的名字。要看出这个条件是必须的，考虑公式 φ（x) 假定为y y ≤ x ("x 是极大的")。如果 t 是没有 y 作为自由变量的项，则 φ（t) 就意味着 t 是极大的。但是，如果 t 是 y 则公式 φ（y) 就是y y ≤ y，这说的不是 y 是极大的。问题是在用 y 替代 φ（x) 中 x 的时候，t (=y) 的自由变量 y 变成了约束的。所以要形成 φ（y) 我们必须首先把 φ 的约束变量 y 改为某个其他变量，比如 z，所以 φ（y) 就是z z ≤ y。忘记这个条件是声名狼籍的犯错误原因。

词汇表

"词汇表"构成如下

谓词变量（或关系）的集合，每个都有某个价（或元数） ≥1，经常指示为大写字母 P,Q,R,...。

常量的集合，经常指示为小写字母，开始于字母 a,b,c,...。

函数的集合，每个都有某个价 ≥ 1，经常指示为小写字母 f,g,h,...。

变量的有限集合，经常指示小写字母，结束于字母 x,y,z,...。

表示逻辑算子（或连结词）的符号： （逻辑非），（逻辑与），（逻辑或），→ （逻辑条件），（逻辑双条件）。

表示量词的符号： （全称量化），（存在量化）.

左和右圆括号。

同一或等于符号 = 有时但不总是在词汇表中。

下面列出一些次要的变化：

基本（primitive）符号（算子和量词）的集合经常变化。有些符号可以被省略并被接受为简写；比如 (P Q) 是 (P → Q) (Q → P) 的简写。在另一方面，有可能包含其他算子作为基本算子，比如真值常量 ("真") 和 ⊥ ("假")（它们是 0 价算子），或Sheffer竖线（P | Q）。需要的基本符号的极小数目是一，但是如果我们把自身限制于上述列出的算子，我们就需要三个；比如 &not；、∧ 和 就足够了。

某些旧的书籍和论文使用符号 φ ψ 表示 φ → ψ，~φ 表示 &not；φ，φ & ψ 表示 φ ∧ ψ，和大量的表示量词的符号；比如x φ 可以被写为 (x）φ。

等式有时被认为是一阶逻辑的一部分；如果是这样，等号包含在词汇表中，而它们的行为在语法上如同二元谓词。这种情况有时叫做有等式的一阶逻辑。

常量实际上同于 0 价的函数，所以有可能并且是便利的省略常量并允许函数有任何价。但是传统上只对至少 1 价的函数使用术语"函数"。

在上述关系的定义中必须有至少 1 价。有可能允许 0 价关系；它们可以被认为是命题变量。

对放置括号有很多不同的约定；例如，你可以写x 或 (?x）。有时使用冒号或句号来替代圆括号使公式免除歧义。一个有趣但非常不常用的约定是"波兰表示法"，这里忽略所有圆括号，在其参数之前写 ∧、∨ 等等，而不是在它们中间。波兰表示法是简约和优雅的，但因为不适合人类阅读而少用。

有一个技术观察，如果有表示有序对的 2 元函数符号（或表示有序对的投影的二元谓词符号），则可以完全分配元数 > 2 的函数或谓词。当然有序对或投影需要满足那些自然公理。

常量、函数和关系的集合通常被认为形成了一个语言，而变量、逻辑算子和量词通常被认为属于逻辑。例如，群论的语言由一个常量（单位元素），一个 1 价函数（反），一个 2 价函数（积），和一个 2 价关系（等于）组成，等号可以被包含在底层的逻辑中而被忽略。

公理

逻辑公理

下面描述一阶逻辑的公理。如上所述，一个给定的一阶理论有进一步的非逻辑公理。下列逻辑公理刻画了本文的样例一阶逻辑的一种演算。

对于任何理论，知道公理的集合是否可用算法生成，或是否存在算法确定合式公式为公理，是很有价值的。

如果存在生成所有公理的算法，则公理的集合被称为递归可枚举的。

如果存在算法在有限步骤后确定一个公式是否是公理，则公理的集合被称为递归的或“可判定的”。在这种情况下，你还可以构造一个算法来生成所有的公理： 这个算法简单的（随着长度增长）一个接一个的生成所有可能的公式，而算法对每个公式确定它是否是个公理。

一阶逻辑的公理总是可判定的。但是在一阶理论中非逻辑公式就不必需如此。

量词公理

下列四个公理是谓词演算的特征：

PRED-1:

PRED-2:

PRED-3:

PRED-4:

它们实际上是公理模式： 表达式 W 表示对于其中任何 wff，x 不是自由的；而表达式 Z(x) 表示对于任何 wff 带有额外的约定，即 Z(t) 表示把 Z(x) 中的所有 x 替代为项 t 的结果。

等式公理

在一阶逻辑中对使用等式（或恒等式）有多种不同的约定。本节总结其中主要的。不同的约定对同样的工作给出本质上相同的结果，区别主要在术语上。

对等式的最常见的约定是把等号包括为基本逻辑符号，并向一阶逻辑增加等式的公理。等式公理是

x = x

x = y → f(...,x,...) = f(...,y,...) 对于任何函数 f

x = y → (P(...,x,...) → P(...,y,...)) 对于任何关系 P （包括 = 自身)

其次常见的约定是把等号包括为理论的关系之一，并向这个理论的公理增加等式的公理。在实际中这是同前面约定最难分辨的，除了在没有等式概念的不常见情况下。公理是一样的，唯一的区别是把它叫做逻辑公理还是这个理论的公理。

在没有函数和有有限数目个关系的理论中，有可能以关系的方式定义等式，通过定义两个项 s 和 t 是相等的，如果任何关系通过把 s 改变为 t 在任何讨论下都没有改变。例如，在带有一个关系 ∈的集合论中，我们可以定义 s = t 为x (s ∈ x t ∈ x) ∧x (x ∈ s x ∈ t) 的缩写。这个等式定义接着自动的满足了关于等式的公理。

在某些理论中有可能给出特别的等式定义。例如，在带有一个关系 ≤ 的偏序的理论中，我们可以定义 s = t 为 s ≤ t ∧ t ≤ s 的缩写。

一阶逻辑的元逻辑定理

下面列出了一些重要的元逻辑定理。

不像命题演算，一阶逻辑是不可判定性的。对于任意的公式 P，可以证实没有判定过程，判定 P 是否有效，（参见停机问题）。（结论独立的来自于邱奇和图灵。）

有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式 P,P 是可证明的。

一元谓词逻辑（就是说，谓词只有一个参数的谓词逻辑）是可判定的。

[编辑] 转换自然语言到一阶逻辑

用自然语言表达的概念必须在一阶逻辑（FOL）可以为为其效力之前必须被转换到 FOL，而在这种转换中可能有一些潜在的缺陷。在 FOL 中， 意味着“要么 p 要么 q 要么二者”，就是说它是“包容性”的。在英语中，单词“or”有时是包容性的（比如，“加牛奶或糖?”），有时是排斥性的（比如，“喝咖啡或茶?”，通常意味着取其中一个或另一个但非二者）。类似的，英语单词“some”可以意味着“至少一个，可能全部”，有时意味着“不是全部，可能没有”。英语单词“and”有时要按“or”转换（比如，“男人和女人可以申请”）。