一阶逻辑

维基百科，自由的百科全书

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

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

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

[编辑] 一阶逻辑的定义

谓词演算构成如下

形成规则(就是形成合式公式的递归定义)。
变换规则(就是推导定理的推理规则)。
公理或公理模式(可能是可数无限的)。

有两种类型的公理: 逻辑公理，它是对于谓词演算有效的，和非逻辑公理，它是在特殊情况下为真的，就是说，在它所在的理论的标准解释中是真的。例如，非逻辑的皮亚诺公理在算术的符号主义标准解释下是真的，但是对于谓词演算它们不是有效的。

在公理的集合是无限的的时候，需要能判定给定的合式公式是否是一个公理的一个算法。进一步的，应当有可以判定一个推理规则的应用是否正确的算法。

[编辑] 词汇表

"词汇表"构成如下

谓词变量(或关系)的集合，每个都有某个价(或元数) ≥1，经常指示为大写字母 P, Q, R,... 。
常量的集合，经常指示为小写字母，开始于字母 a, b, c,...。
函数的集合，每个都有某个价 ≥ 1，经常指示为小写字母 f, g, h,... 。
变量的有限集合，经常指示小写字母，结束于字母 x, y, z,...。
表示逻辑算子(或连结词)的符号: $\neg$ (逻辑非), $\wedge$ (逻辑与), $\vee$ (逻辑或), → (逻辑条件), ↔ (逻辑双条件)。
表示量词的符号: $\forall$ (全称量化), $\exists$ (存在量化).
左和右圆括号。
同一或等于符号 = 有时但不总是在词汇表中。

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

基本(primitive)符号(算子和量词)的集合经常变化。有些符号可以被省略并被接受为简写；比如 (P ↔ Q) 是 (P → Q) $\wedge$ (Q → P) 的简写。在另一方面，有可能包含其他算子作为基本算子，比如真值常量 ⊤ ("真") 和 ⊥ ("假")(它们是 0 价算子)，或Sheffer竖线(P | Q)。需要的基本符号的极小数目是一，但是如果我们把自身限制于上述列出的算子，我们就需要三个；比如 ¬、∧ 和 ∀ 就足够了。
某些旧的书籍和论文使用符号 φ ⊃ ψ 表示 φ → ψ，~φ 表示 ¬φ，φ & ψ 表示 φ ∧ ψ，和大量的表示量词的符号；比如 ∀x φ 可以被写为 (x)φ。
等式有时被认为是一阶逻辑的一部分；如果是这样，等号包含在词汇表中，而它们的行为在语法上如同二元谓词。这种情况有时叫做有等式的一阶逻辑。
常量实际上同于 0 价的函数，所以有可能并且是便利的省略常量并允许函数有任何价。但是传统上只对至少 1 价的函数使用术语"函数"。
在上述关系的定义中必须有至少 1 价。有可能允许 0 价关系；它们可以被认为是命题变量。
对放置括号有很多不同的约定；例如，你可以写 ∀x 或 (∀x)。有时使用冒号或句号来替代圆括号使公式免除歧义。一个有趣但非常不常用的约定是"波兰表示法"，这里忽略所有圆括号，在其参数之前写 ∧、∨ 等等，而不是在它们中间。波兰表示法是简约和优雅的，但因为不适合人类阅读而少用。
有一个技术观察，如果有表示有序对的 2 元函数符号(或表示有序对的投影的二元谓词符号)，则可以完全分配元数 > 2 的函数或谓词。当然有序对或投影需要满足那些自然公理。

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

[编辑] 形成规则

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

[编辑] 项

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

任何常量是项。
任何变量是项。
n ≥ 1 个参数的任何表达式 f(t₁,...,t_n) (这里的每个参数 t_i 都是项，而 f 是 n 价的函数符号) 是项。
闭包条款: 其他东西都不是项。

[编辑] 合式公式

合式公式(通常叫做 wff 或只是公式)按如下规则递归的定义:

简单和复杂谓词 如果 P 是 n ≥ 1 价的关系而 a_i 是项，则 P(a₁,...,a_n) 是合式的。如果等式被认为是逻辑的一部分，则 (a₁ = a₂) 是合式的。所有这个公式都被称为是原子。
归纳条款 I: 如果 φ 是 wff，则 ¬φ 是 wff。
归纳条款 II: 如果 φ 和 ψ 是 wff，则 (φ → ψ) 是 wff。
归纳条款 III: 如果 φ 是 wff 而 x 是变量，则 ∀x φ 是 wff。
闭包条款: 其他东西都不是 wff。

因为 ¬(φ → ¬ψ) 逻辑等价于 (φ ∧ ψ)，(φ ∧ ψ) 经常用做简写。(φ ∨ ψ) 和 (φ ↔ ψ) 也是同样的道理。还有 ∃x φ 是 ¬∀y ¬φ 的简写。实际中，如果 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 在 ¬φ 中是自由的，当且仅当 x 在 φ 中是自由的。
归纳条款 II: x 在 (φ → ψ) 中是自由的，当且仅当 x 在 φ 中是自由的或者 x 在 ψ 中是自由的。
归纳条款 III: x 在 ∀y φ 中是自由的，当且仅当 x 在 φ 中是自由的并且 xǂy。
闭包条款: 如果 x 在 φ 中不是自由的，则它是约束的。

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

[编辑] 例子

有序阿贝尔群的语言有一个常量 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
(∀x ∃y ≤( +(x, y), z)) ∧ (∃x =(+(x, y), 0)) 是公式，通常写为 (∀x ∃y 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。忘记这个条件是声名狼籍的犯错误原因。

[编辑] 推理规则

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

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

$\mathit{if} \vdash Z(x), \mathit{then} \vdash \forall x Z(x)$

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

[编辑] 公理

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

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

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

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

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

[编辑] 量词公理

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

PRED-1: $\forall x Z(x) \rightarrow Z(t)$
PRED-2: $Z(t) \rightarrow \exists x Z(x)$
PRED-3: $\forall x (W \rightarrow Z(x)) \rightarrow (W \rightarrow \forall x Z(x))$
PRED-4: $\forall x (Z(x) \rightarrow W) \rightarrow (\exists x Z(x) \rightarrow W)$

它们实际上是公理模式: 表达式 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 的缩写。

[编辑] 谓词演算

谓词演算是命题演算的扩展，它定义了哪些一阶逻辑的陈述是可证明的。它是用来描述数学理论的形式系统。如果命题演算用一组合适的公理和一个单一的推理规则肯定前件来定义（可以有很多不同的方式），则谓词演算可以通过增加一些补充的公理和补充的推理规则"全称普遍化"来定义。更精确的说，谓词演算采用的公理有:

来自命题演算的所有重言式（命题变量被替代为公式）。
上面给出的量词公理。
上面给出的等式公理，如果等式被认为是逻辑概念的话。

一个句子被定义为是在一阶逻辑中可证明的，如果可以通过从谓词演算的公理开始并重复应用推理规则"肯定前件"和"全称普遍化"来得出它。

如果我们有一个理论 T （在某些语言中叫做公理的陈述的集合），则一个句子 φ 被定义为是在理论 T 中可证明的，如果

a ∧ b ∧ ... → φ

在一阶逻辑中对于理论 T 的某个公理 a, b,... 的有限集合是可证明的。

可证明性的一个明显问题是它好象非常特别: 我们采用了显然随机的公理和推理规则的搜集，不清楚是否意外的漏掉了某个关键的公理或规则。哥德尔完备性定理确保这实际上不是问题: 这个定理声称在所有模型中为真的任何陈述在一阶逻辑中都是可证明的。特别是，在一阶逻辑中"可证明性"的任何合理定义都必须等价于上述定义(尽管在不同的可证明性的定义下证明的长度可能有巨大差别)。

有很多不同（但等价）的方式来定义可证明性。前面的演算是"希尔伯特风格"演算的一个典型例子，它有许多不同的公理但只有非常少的推理规则。"根岑风格"谓词演算有非常少的公理但有许多推理规则。

文法上说谓词演算在现存的命题演算上增加了“谓词-主词结构”和量词。主词是给定的个体群组(集合)的一个成员的名字，而谓词是在这个群组上的关系，一元谓词在哲学中称为性质，在数学中称为指示函数，在数理逻辑中称为布尔值函数。

[编辑] 可证明的恒等式

$\neg \forall x P(x) \Leftrightarrow \exists x \neg P(x)$

$\neg \exists x P(x) \Leftrightarrow \forall x \neg P(x)$

$\forall x \forall y P(x,y) \Leftrightarrow \forall y \forall x P(x,y)$

$\exists x \exists y P(x,y) \Leftrightarrow \exists y \exists x P(x,y)$

$\forall x P(x) \land \forall x Q(x) \Leftrightarrow \forall x (P(x) \land Q(x))$

$\exists x P(x) \lor \exists x Q(x) \Leftrightarrow \exists x (P(x) \lor Q(x))$

[编辑] 可能增加的推理规则

$\exists x \forall y P(x,y) \Rightarrow \forall y \exists x P(x,y)$

$\forall x P(x) \lor \forall x Q(x) \Rightarrow \forall x (P(x) \lor Q(x))$

$\exists x (P(x) \land Q(x)) \Rightarrow \exists x P(x) \land \exists x Q(x)$

$\exists x P(x) \land \forall x Q(x) \Rightarrow \exists x (P(x) \land Q(x))$

[编辑] 一阶逻辑的元逻辑定理

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

不像命题演算，一阶逻辑是不可判定性的。对于任意的公式 P，可以证实没有判定过程，判定 P 是否有效，(参见停机问题)。(结论独立的来自于邱奇和图灵。)
有效性的判定问题是半可判定的。按哥德尔完备性定理所展示的，对于任何有效的公式 P, P 是可证明的。
一元谓词逻辑(就是说，谓词只有一个参数的谓词逻辑)是可判定的。

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

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

[编辑] 一阶逻辑的限制

所有数学概念都有它的强项和弱点；下面列出一阶逻辑的一些问题。

[编辑] 难于表达 if-then-else

太奇怪了，(如典型定义的)带有等式的 FOL 不包含或允许定义 if-then-else 谓词或函数 if(c,a,b)，这里的 c 是表达为公式的条件，而 a 和 b 是要么都是项要么都是公式，并且它的结果是 a 如果 c 为真，或者 b 如果它为假。问题在于 FOL 中，谓词和函数二者只接受(“非布尔类型”)项作为参数，而条件的明确表达是(“布尔类型”)公式。这是不幸的，因为很多数学函数是依据 if-then-else 而方便的表达的，而 if-then-else 是描述大多数计算机程序的基础。

在数学上，有可能重定义匹配公式算子的新函数的完备集合，但是这是非常笨拙的。^[3] 谓词 if(c,a,b) 如果重写为 $(c \wedge a) \or (\neg c \wedge b)$ 就可以在 FOL 中表达，但是如果条件 c 是复杂的这就是笨拙的。很多人扩展 FOL 增加特殊情况谓词叫做“if(条件, a, b)”(这里 a 和 b 是公式)和/或函数“ite(条件, a, b)”(这里的 a 和 b 是项)，它们都接受一个公式作为条件，并且等于a 如果条件为真，或 b 如果条件为假。这些扩展使 FOL 易于用于某些问题，并使某类自动定理证明更容易。^[4] 其他人进一步扩展 FOL 使得函数和谓词可以在任何位置接受项和公式二者。

[编辑] 类型(种类)

除了在公式(“布尔类型”)和项(“非布尔类型”)之间的区别之外，FOL 不包括类型(种类)到自身的概念中。某些人争辩说缺乏类型是巨大优点 ^[5]，而很多其他人发觉了定义和使用类型(种类)的优点，比如帮助拒绝某些错误或不想要的规定 ^[6]。想要指示类型的那些人必须使用在 FOL 中可获得的符号来提供这种信息。这么做使得这种表达更加复杂，并也容易导致错误。

单一参数谓词可以用来在合适的地方实现类型的概念。例如:

$\forall x Man(x) \rightarrow Mortal(x)$ ，

谓词 Man(x) 可以被认为是一类“类型断言”(就是说，x 必须是男人)。谓词还可以同指示类型的“存在”量词一起使用，但这通常应当转而与逻辑合取算子一起来做，比如:

$\exists x Man(x) \wedge Mortal(x)$ (“存在既是男人又是人类的事物”)。

容易写成 $\exists x Man(x) \rightarrow Mortal(x)$ ，但这将等价与 $\exists x \neg Man(x) \or \exists x Mortal(x)$ (“存在不是男人的事物或者存在是人类的事物”)，这通常不是想要的。类似的，可以做一个类型是另一个类型的子类型的断言，比如:

$\forall x Man(x) \rightarrow Mammal(x)$ (“对于所有 x, 如果 x 是男人，则 x 是哺乳动物)。

[编辑] 难于刻画有限性或可数性

主条目：二阶逻辑

从 Löwenheim–Skolem定理得出在一阶逻辑中不可能刻画有限性或可数性。例如，在一阶逻辑中你不能断言实数的集合的上确界性质，它声称实数的所有有界的、非空集合都有上确界；这就需要二阶逻辑了。

[编辑] 图可及性不能表达

很多情况可以被建模为节点和有向连接(边)的图。例如，效验很多系统要求展示不能从“好”状态触及到“坏”状态，而状态的相互连接经常可以建模为图。但是，可以证明这种可及性不能用谓词逻辑完全表达。换句话说，没有谓词逻辑公式 f，带有 u 和 v 作为它的唯一自由变量，而 R 作为它唯一的(2 元)谓词符号，使得 f 在一个有向图中成立，如果在这个图中存在从关联于 u 的节点到关联于 v 的节点的路径。^[7]

[编辑] 引用

^ For another well-worked example, see Metamath proof explorer
^ Suber, Peter, Translation Tips. Retrieved on 2007-09-20
^ Otter Example if.in. Retrieved on 2007-09-21
^ Manna, Zohar (1974), Mathematical Theory of Computation, New York, New York: McGraw-Hill Book Company, ISBN 0-07-039910-7, at 77-147
^ Leslie Lamport, Lawrence C. Paulson. Should Your Specification Language Be Typed? ACM Transactions on Programming Languages and Systems. 1998. http://citeseer.ist.psu.edu/71125.html
^ Rushby, John. Subtypes for Specification. 1997. Proceedings of the Sixth European Software Engineering Conference (ESEC/FSE 97). http://citeseer.ist.psu.edu/328947.html
^ Huth, Michael & Mark Ryan (2004), Logic in Computer Science, 2nd edition, ISBN 0-521-54310-X, at 138-139

Jon Barwise and John Etchemendy, 2000. Language Proof and Logic. CSLI (University of Chicago Press) and New York: Seven Bridges Press.
David Hilbert and Wilhelm Ackermann 1950. Principles of Theoretical Logic (English translation). Chelsea. The 1928 first German edition was titled Grundzüge der theoretischen Logik.
Wilfrid Hodges, 2001, "Classical Logic I: First Order Logic," in Lou Goble, ed., The Blackwell Guide to Philosophical Logic. Blackwell.

[编辑] 参见

[编辑] 外部链接

Stanford Encyclopedia of Philosophy: "Classical Logic -- by Stewart Shapiro. Covers syntax, model theory, and metatheory for first order logic in the natural deduction style.
forall x: an introduction to formal logic, by P.D. Magnus, covers formal semantics and proof theory for first-order logic.
Metamath: an ongoing online project to reconstruct mathematics as a huge first order theory, using first order logic and the axiomatic set theory ZFC. Principia Mathematica modernized and done right.
Podnieks, Karl. Introduction to mathematical logic.

来自“http://zh.wikipedia.org/wiki/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91”

分类: 數理邏輯 | 形式逻辑系统