一阶逻辑

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

一阶谓词演算或一阶逻辑(FOL)允许量化陈述的公式，比如"存在着 x，..." ( $\exists x$ ) 或 "对于任何 x，..." ( $\forall x$ )，这里的 x 是论域的成员。一阶(递归)公理化理论是通过把一阶句子/断定的递归可枚举集合增加为公理，可以被公理化为一阶逻辑扩展的理论。这里的"..."叫做谓词并表达某种性质。谓词是适用于某些事物的表达。所以，表达"是黄色"或"喜欢椰菜"分别适用于是黄色或喜欢椰菜的那些事物。一阶逻辑不允许量化性质，不能表达下列陈述，"对于所有的性质 P，..." 或"存在着性质 P，..."。

但是，一阶逻辑足够强大了，它可以形式化全部的集合论和几乎所有的数学。把量化限制于个体(individual)使它难于用于拓扑学目的，但它是在数学底层经典的逻辑理论。它是比句子逻辑强比二阶逻辑弱的理论。同时，由于利用集合论中的一些工具可以实现对某些性质量化的目的（例如，把具有某些性质的对象抽象为集合，然后对这些集合进行量化），因此它的能力并不明显地比二阶逻辑弱。然而某些重要的性质（例如关于基数和序数的某些性质）由于在集合论中不能抽象出集合，因此仍然无法量化。同时，即使可以这样做，它们也只不过是赝品。

[编辑] 一阶逻辑的定义

谓词演算构成如下

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

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

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

[编辑] 词汇表

"词汇表"构成如下

谓词变量(或关系)的集合，每个都有某个价(或元数) ≥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 在 φ 中是自由的，当且仅当 x 出现在 φ 中。
归纳条款 I: x 在 ¬φ 中是自由的，当且仅当 x 在 φ 中是自由的。
归纳条款 II: x 在 (φ → ψ) 中是自由的，当且仅当 x 在 φ 中是自由的或者 x 在 ψ 中是自由的。
归纳条款 III: x 在 ∀y φ 中是自由的，当且仅当 x 在 φ 中是自由的并且 xǂy。
闭包条款: 如果 x 在 φ 中不是自由的，则它是约束的。

因为 ¬(φ → ¬ψ) 逻辑等价于 (φ ∧ ψ)，(φ ∧ ψ) 经常用做简写。(φ ∨ ψ) 和 (φ ↔ ψ) 也是同样的道理。还有 ∃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))) 。

例子: 有序阿贝尔群的语言有一个常量 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。忘记这个条件是声名狼籍的犯错误原因。

[编辑] 等式

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

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

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 的缩写。

[编辑] 推理规则

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

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

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

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

注意：全称普遍化类似于模态逻辑的必然性规则，它是

$\mathit{if} \vdash P, \mathit{then} \vdash \Box P$

[编辑] 量词公理

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

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 的结果。

[编辑] 谓词演算

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

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

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

如果我们有一个理论 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 是可证明的。
单体谓词逻辑(就是说，谓词只有一个参数的谓词逻辑)是可判定的。

[编辑] 引用

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../../../%E4%B8%80/%E9%98%B6/%E9%80%BB/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91.html”

页面分类: 數理邏輯

一阶逻辑

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

目录

[编辑] 一阶逻辑的定义

[编辑] 词汇表

[编辑] 形成规则

[编辑] 代换

[编辑] 等式

[编辑] 推理规则

[编辑] 量词公理

[编辑] 谓词演算

[编辑] 恒等式

[编辑] 推理规则

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

[编辑] 引用

[编辑] 参见

[编辑] 外部链接

Views

导航

帮助

搜索

其他语言