Lecture

谓词逻辑

• 需要更丰富的语言

• 谓词逻辑作为一种形式语言

  • 术语-变量、函数

  • 公式-谓词、量词

  • 自由变量和约束变量

  • 替代

• 谓词逻辑的证明理论

  • 自然演绎规则

需要更丰富的语言

命题逻辑：

研究陈述句，关于世界的陈述，这些陈述可以被赋予真理值

能很好地处理句子成分，如：not，and，or，if then

限制：无法处理修改器，如存在、全部、中间、仅。

例子：“每个学生都比一些老师年轻。”

我们可以用命题符号p来识别整个短语。

然而，这个短语有更精细的逻辑结构。它是关于以下属性的声明：

• 作为一名学生

• 当讲师

• 比别人年轻

谓词、变量和量词

属性由谓词表示。S、 I，Y是谓词。

• S(andy)：安迪是个学生。

• I(paul)：保罗是一名教师。

• Y(andy,paul)：安迪比保罗年轻。

变量是具体值的占位符。

• S(x):x是一名学生。

• I(x):x是一名教师。

• Y(x,y):x比Y年轻。

量词可以对短语进行编码：

“每个学生都比一些老师年轻。”

两个量词：-forall和-exists。

上述句子的编码：

More Examples

没有书是气态的。字典是书。因此，没有字典是气态的。

我们表示：B(x):x是一本书

G(x):x是气态的

D(X):x是一本字典

“每个孩子都比他母亲小”

我们表示：C(x):x是一个孩子

M(x,y):x的妈妈是y

表示m(x)：x的母亲

因为每个人都有一个独特的母亲，所以使用函数m来编码“母亲”关系更合适。

“安迪和保罗有同一个外祖母”

我们引入了一个新的特殊谓词：相等。

备选代表： m(m(a)) = m(m(p)) 考虑关系B(x,y): x是Y的兄弟。这种关系必须编码为谓词，因为一个人可能有多个兄弟。

谓词逻辑作为一种形式语言

谓词公式中的两类“事物”：

• 对象，例如a（Andy）和p（Paul）。功能符号也指对象。这些都是用术语建模的。

• 可以给定真值的表达式。这些都是通过公式建模的。

谓词词汇表由3组组成：

• 谓词符号P；

• 功能符号F

• 常数C。

每个谓词和函数符号都有一个固定的arity（即参数数量）

谓词逻辑的形式语言元素：

• 项

• 公式

• 自由约束变量

• 替代

项

定义：项定义如下：

• 任何变量都是一个术语；

• C中的任何常数都是一个项；

• 如果是项，f∈F有算术数n，那么是项；

• 没有其他东西是一个术语。

巴克斯·诺尔定义： ，其中x表示变量，c表示C中的常数，f表示F中的函数，arity为n。

评论：

术语的第一个构建块是常量和变量。

更复杂的术语是使用以前构建的术语从函数符号构建的。

术语的概念独立于集合C和F

函数

定义：我们使用已经定义的F上的术语集，归纳地定义（F，P）上的公式集。

• 如果P是一个有n≥1个参数的谓词， 是F上的项，那么是一个公式。

• 如果Φ是一个公式，那么也是一个公式

• 如果Φ和ψ是公式，那么也是公式

• 如果Φ是一个公式，x是一个变量，那么和就是公式。

没有其他东西是公式。

BNF定义：

其中P是arity n的谓词，是项，，x是变量。

约定：我们保留了连接词通常的绑定优先级，我们添加了和 绑定，如。

例子

考虑翻译句子：

“我父亲的每个儿子都是我的兄弟”

两个备选方案：

• “父亲”关系编码为谓词。

S(x,y):x是y的儿子。

F(x,y):x是y的父亲。

B(x,y):x是y的兄弟。

m：常量，表示“我自己”。

翻译：

• “父亲”关系编码为函数。

f(x):x的父亲。

翻译：

自由和约束变量

定义：设Φ为谓词逻辑中的公式。如果Φ中的x是Φ的解析树中的叶节点，那么Φ中的x的出现在Φ中是自由的，因此从该节点x到节点 或 没有向上的路径。否则，该事件x称为绑定。对于 ，我们说Φ-减去它的任何子公式，或-分别是,的范围

自由变量和约束变量示例

替代

变量是占位符，所以我们必须有办法用更具体的信息替换它们。

定义：给定一个变量x、一个项t和一个公式Φ，我们将定义为用t替换Φ中每个自由出现的变量x得到的公式。

定义：给定一个项t、一个变量x和一个公式Φ，我们说，对于t中出现的每个变量y，如果Φ中没有自由x叶出现在或范围内，那么t对于Φ中的x是自由的。

备注：如果t对Φ中的x不自由，则替换具有不必要的影响。

例子： 通过将重命名为来避免这种情况。

谓词逻辑的证明理论

• 命题逻辑的自然推理规则仍然有效

• 谓词逻辑的自然推理规则：

  • 命题逻辑的证明规则；

  • 平等的证明规则；

  • 通用量化的证明规则；

  • 存在量化的证明规则。

• 量词等价

平等的证明规则

约定：当我们以的形式写一个替换时，我们隐式地假设t对于Φ中的x是自由的

证明实例：

Solution

通用量化的证明规则

证明实例：

Solution

Solution

存在量化的证明规则

证明实例：

Solution

Solution

Another Example

Solution

Assignment

用演绎规则证明下列定理

(1)∀x(P(x) → ¬Q(x)) ⊢ ¬(∃x(P(x)∧Q(x)))

Solution

(2)∀x(P(x) ↔ x=b) ⊢ P(b)∧∀x∀y(P(x)∧P(y) → x=y)

Solution