谓词#

个体变量和谓词#

简单命题 = 主语（独立存在的客体） + 谓语（形容客体性质和客体之间关系的部分）

• 个体词
  • 个体常量：表示具体的个体词
  • 个体变量：表示泛指的个体词
• 个体域：个体词的取值范围
• 全总个体域：所有个体域构成的个体域。

n元谓词：在非空个体域D上，定义在$D^n$上的值域为{0, 1}的n元函数，记为$P(x_1, x_2, ..., x_n)$； 其中，个体变量$x_1, x_2, ..., x_n \in D$

• 谓词常量：表示具体性质或关系的谓词
• 谓词变量：表示抽象或泛指性质的谓词

谓词中个体词的顺序不能变更。

1元谓词表示一个个体的特性，n元谓词表示n个个体之间的关系。

谓词本身并不是命题，只有用谓词常量和个体常量代替之后才是命题。

量词#

• 全称量词$(\forall)$:作为蕴含条件式的前提

• 存在量词$(\exist)$：作为合取式的合取项

谓词逻辑符号化

1. 天下乌鸦一般黑； $F(X): x \in crow; G(x, y):x, y \space are \space black$

则命题符号化为： $(\forall x)(\forall y)(F(x) \land F(y) \rightarrow G(x, y))$

或$\neg (\exist x)(\exist y)(F(x) \land F(y) \land \neg G(x, y))$

2. 每个实数都存在比它大的另外的实数 $R(x)：x \in R; L(x, y): x < y$

则命题符号化为：$(\forall x)(R(x) \rightarrow (\exist y)(R(y) \land L(x, y)))$

谓词公式#

• 常量符号： 个体域D的某个元素

• 变量符号： 个体域D的任意元素

• 函数符号： 在个体域集合内，个体域到另一个个体域个体词的变化。（代替蕴含式），用小写字母表示

• 谓词符号：表示个体域集合内D^n -> {0, 1}的任意一个谓词。用大写字母表示。

• 项：由任意的常量符号或者变量符号通过有限次函数符号组合而成。

合式公式#

• 原子公式：由n元谓词，和项组成的原子谓词。

• 合式公式：由有限个合式公式组合而成。

原子公式是合式公式

联结词连接的合式公式也是合式公式

由量词连接的合式公式也是合式公式

自由变元与约束变元#

• 给定一个公式G，若变元x出现在使用变元的两次的辖域之内，则称变元x的出现为约束出现，此时x称为约束变元。反之称为自由变元。
  • 辖域：若量词后有括号，则括号内的子公式就是该量词的辖域。$(\forall x)(...)$
  • 没有括号，辖域的范围就是相邻的公式。$(\forall x)P(x)G(y)$，y为自由变元。

修改约束变元时，需要修改辖域内的所有约束变元 对于自由变元，应当使用新的符号进行替换。

• 闭式：公式G中没有自由出现的个体变元（都是约束变元），称为封闭的合式公式。

谓词公式的解释#

谓词公式G的解释I由如下四部分组成：

1. 非空的个体域集合D
2. G中的每个常量符号
3. G中的每个n元函数符号，指定由D^n -> D中的某个特定函数。
4. G中的每个n元谓词符号，指定由D^n -> {0, 1}

• 举例：

基本等价公式：

1. 量词可以任意在辖域的括号内外切换，只影响约束变元。
2. 对于同一个谓词公式，多个量词公式的顺序可以交换。

• 量词分配律

$(\forall x) (G(x) \land H(x)) == (\forall x)G(x) \land (\forall) H(x)$​

$(\exist x)(G(x) \lor H(x)) == (\exist x)G(x) \lor (\exist x)H(x)$

谓词和命题的区别#

• 命题公式：不含量词的公式
• 谓词公式：具有量词的公式

推理形式和推理规则#

设$G_n, H$是公式，H是G的逻辑结果当且仅当对任意解释I，若I同时满足G_n，则I满足H。记为:$G_1, G_2, ..., G_n \implies H$，此时称$G_1, G_2, ..., G_n \implies H$是有效的，否则是无效的。

可以把$G_1, G_2, ..., G_n$这一组前提(premise)用集合$\Gamma$表示。称H为结论(conclusion)。

H是前提集合$\Gamma$的逻辑结果$\Gamma \implies H$，当且仅当$G_1 \land G_2 \land ... \land G_n \rightarrow H$为有效公式。

推理规律#

$I_{13}: (\forall x)G(x) \lor (\forall x)H(x) \implies (\forall x)(G(x) \lor H(x))$

$I_{13}: (\exist x)G(x) \land (\exist x)H(x) \implies (\exist x)(G(x) \land H(x))$

将个体域缩小

• 全称特指规则UG

描述整体需要量词，描述个体不需要量词 当需要从整体与个体之间的过渡时，需要消去或添加量词

$(\forall x)G(x) \implies G(y)$，y不再G(x)中约束出现

$(\forall x)G(x) \implies G(c)$，c为任意个体常量

全称量词 -> 常量变元 全称量词 -> 自由变元

• 存在特指规则ES

$(\exist x)G(x) \implies G(c)$，c为使G(c)为真的特定的个体常量

当G(x)中还有除x之外的自由变元(如：y)，使用关于这些变元(y)的函数符号来取代c(如：f(y))

存在量词 -> 自由变元的函数

• 全称推广规则UC

$G(y) \implies (\forall x)G(x), G(y)$中无变元x

自由变元 -> 全称量词

• 存在推广规则

$G(c) \implies (\exist x) G(x)$，c为特定个体常量

或：$G(y) \implies (\exist x)G(x), G(y)$中无变元x

常量变元 -> 存在量词 自由变元 -> 存在量词

推理三部曲#

• 举例：

需要同时使用规则US和规则ES消去同一个符号的量词时，必须先使用规则ES，再使用规则US。

使用规则ES消去量词后，对该变量添加量词只能用EG；而US消去的既可以用UG也可以用EG

使用UG、EG时，必须是前束范式。

CP规则证明法#

• 思路

将析取变化为蕴含式再证明；蕴含式的前件为前提，蕴含式的后件为结果。

• 结果

反证法#

将结果的非，引入为附加前提P

• 推导