谓词演算

数理逻辑形式系统

谓词演算是数理逻辑最基本的形式系统，其又被称为一阶逻辑。一个可以回答真假的命题，不仅可以分析到简单命题，还可以分析到其中的个体、量词和谓词全称量词表示“每一个” 。公式∃ x(P(x)∧Q(x))表示存在有叶子的树，∃这里是存在量词，表示“至少存在一个”。

基本介绍

谓词演算除了一元谓词，也可以有二元，三元，甚至多元谓词。事实上，数学中的关系，函数都可以看成谓词。例如x≤y可以看成二元谓词，x+y=z可以看成三元谓词，因此谓词演算的公式可表示数学中的一些命题。

谓词可以在一定的个体集合中给出解释，谓词公式可以在这样的个体集合中取到真假值。例如（*）在实数集R中解释Q(x)为x是有理数，则谓词公式（*）取值为真。如果在R中解释Q(x)为“x是整数”，谓词公式（*）就取值为假了。

谓词公式在个体集合中取值的严格定义称为基本语义定义，这个定义是波兰籍数学家A.塔尔斯基在20 世纪 30年代给出的。给定了谓词解释的个体集合称为模型。基本语义定义使谓词公式和模型都可以被当作数学对象加以研究。一个谓词公式在任意一个模型中都取真值，就称之谓恒真式。两个谓词公式A，B在任意模型的任何一种解释下都取相同的值，就称A，B逻辑等价。命题演算中的恒真式和等价式所反映的规律在谓词演算中仍成立。利用有关量词的等价式作等价变换，可以把任何一个谓词公式的量词移到公式的最前面，得到与之等价的前束标准形公式。

推演规则

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

①全称量词消去(UI) ②全称量词引入(UG)

③存在量词消去(EI) ④存在量词引入(EG)

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

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

公理

谓词演算的公理系统可引申到逻辑公理，命题演算公理等其它相关公理，按照这个顺序，我们来介绍如下的公理系统。

构成

谓词演算公理系统的构成：

（1）符号库（初始符号）

（2）形成规则（符号的使用）

（3）公理（推演的起点）

（4）变形规则（推演规则）

逻辑公理

下面描述谓词演算中的一阶逻辑公理。一个给定的一阶理论有进一步的非逻辑公理。

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

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

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

命题演算公理

下列五个公理被成为命题演算公理系统：

图1的14条公理分成五组，在每一组符号中均出现蕴含号，而且还都是蕴含式，即公式形成时最后一次为蕴含运算。五组公理第一组中不再有其他符号，其余四组依次出现一个新符号，它们是合取&析取V否定--和等价号（即～）。

注意，这14条公理显然都是第一章命题逻辑中的永真公式，如果读者怀疑其永真性，不妨用真值表方法去验证一下。但是我希望读者能直接看出每一条都是一个永真命题，即所谓的“重言式”。

等式公理

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

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

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

元逻辑定理

关于一阶逻辑的重要的元逻辑结果有：

①可靠性定理，即凡定理都是普遍有效的。　②一致性定理。一阶逻辑是一致的。若取只有一个个体a的集为论域，αA(α)即为A(a)，而所有量词全部消去。于是，所有的公式都可看作是命题演算的公式。因此，对任一公式A，不可能A和非A都可证。

③完全性定理。一阶逻辑在语义意义下是完全的，即凡普遍有效的公式都是定理。完全性定理还有一个更强的形式，即每一一致的公式集都有模型，都是可满足的。这一更强形式的完全性定理也称强完全性。

④紧致性定理。一个公式集г是有模型的,当且仅当它的每一有穷子集是有模型的。根据一个比较容易证明的定理，公式集г是一致的,当且仅当它的每一有穷子集是一致的。紧致性定理能直接从完全性定理推出。

可判定定理

谓词演算最主要是在一阶谓词上的运算，下面列出了相关的一些重要的关于是否可判定的元逻辑定理。

不像命题演算，一阶逻辑是不可判定性的。对于任意的公式 P，可以证实没有判定过程，判定 P 是否有效，（参见停机问题）。

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

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

全国各地天气预报查询