量词是谓词逻辑的核心元素，表示对某些元素的声明。

• 存在量词 (Existential Quantifier) ∃

• 全称量词 (Universal Quantifier) ∀

 

• means that is a child

• means that is ’s mother

• means that is younger than

自然演绎

The rule for equality

Here equality in terms of computation results.

In either of these senses, any term has to be equal to itself.

The rule for universal quantification

(forall)

The rule for eliminating is the following:

• If is true, then you could replace the in by any term and conclude that is true as well.
• 符号 表示一个替换的操作，其中将 中的所有 替换为

• “所有的水果都是健康的食物”【∀x (x 是水果 → x 是健康的食物)】。如果现在有一个苹果，则可以得出结论：“这个苹果是健康的食物”，因为苹果是水果的一个特定实例。

The rule for introducing is the following:

• If, starting with a ‘fresh’ variable , you are able to prove some formula with in it, then (because is fresh) you can derive .

• 有一种全新的水果种类 “FruitX”。它被发现含有丰富的维生素C（φ[FruitX/x]）。由于 “FruitX” 是一个未知的水果，那么可以推广这个结论，得出 “所有水果都含有丰富的维生素C”（∀x φ）。这里重要的点是，“FruitX”是任意的，没有使用任何特殊的信息来证明它含有维生素C。

---

Example: Prove that

Example: Prove that for any term t

The rule for existential quantification

(exist)

The rule for introducing is the following:

• 如果知道一个具体实例 满足某个性质 ，那么可以得出一个结论：至少存在一个 满足这个性质。也就是说，从一个具体例子推广到一个更一般的存在性声明。

• 假设发现了一种特殊的苹果，它是彩色的。表示 表示“是彩色的苹果”， 表示这个具体的苹果。因为你有一个具体的彩色苹果，所以你可以说 “存在至少一个彩色的苹果”（）。

The rule for eliminating is the following:

• 它允许假设有一个具体的实例 ，满足性质 ，然后使用这个假设去证明其他结论
• 证明 时不能依赖于 的具体身份，这样 才能在去掉存在性假设后独立成立。

• 为了证明 “存在一个人能跑得比闪电还快”（）。在逻辑上，可以假设有这样一个人，称他为“速度先生”（）。如果能用这个假设推导出一些不依赖于 "速度先生" 身份的结论，比如说 “超人速度的存在可能性”，那么这个结论在逻辑上是有效的，即使我们不知道 “速度先生” 究竟是谁。

Example: Prove that

Example: Prove that

• The formula ∃xQ(x) in line 6 is the instantiation of χ in the rule ∃e and does not contain an occurrence of x0, so it is allowed to leave the box to line 7.