Predicate logic,也称一阶逻辑 (First-order logic)
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2F8f6adb06-7a5c-4191-8cf7-772b389f91c9%2FUntitled.png?table=block&id=9a73fd0f-1ed5-42a7-ad4d-0ec78197d666&t=9a73fd0f-1ed5-42a7-ad4d-0ec78197d666&width=288&cache=v2)
量词是谓词逻辑的核心元素,表示对某些元素的声明。
- 存在量词 (Existential Quantifier)
∃
- 全称量词 (Universal Quantifier)
∀
E.g. Every child is younger than its mother.
- 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.
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2Fe06c9610-a087-48c0-a1bf-4afd86ddecc4%2FUntitled.png?table=block&id=5489dd0d-3a1a-4c07-8232-f202dc6be17d&t=5489dd0d-3a1a-4c07-8232-f202dc6be17d&width=96&cache=v2)
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
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2F9c7f9e74-8073-4c95-9851-9103305c7a36%2FUntitled.png?table=block&id=06a40343-d96a-4db3-a0e1-c1c151323411&t=06a40343-d96a-4db3-a0e1-c1c151323411&width=432&cache=v2)
Example: Prove that for any term t
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2Ffe5597d2-e670-4b9c-9760-23cdbd550280%2FUntitled.png?table=block&id=99acfb02-4149-4058-9b0e-d78cd2a30d48&t=99acfb02-4149-4058-9b0e-d78cd2a30d48&width=432&cache=v2)
The rule for existential quantification
(exist)
The rule for introducing is the following:
- 如果知道一个具体实例 满足某个性质 ,那么可以得出一个结论:至少存在一个 满足这个性质。也就是说,从一个具体例子推广到一个更一般的存在性声明。
- 假设发现了一种特殊的苹果,它是彩色的。表示 表示“是彩色的苹果”, 表示这个具体的苹果。因为你有一个具体的彩色苹果,所以你可以说 “存在至少一个彩色的苹果”()。
The rule for eliminating is the following:
- 它允许假设有一个具体的实例 ,满足性质 ,然后使用这个假设去证明其他结论
- 证明 时不能依赖于 的具体身份,这样 才能在去掉存在性假设后独立成立。
- 为了证明 “存在一个人能跑得比闪电还快”()。在逻辑上,可以假设有这样一个人,称他为“速度先生”()。如果能用这个假设推导出一些不依赖于 "速度先生" 身份的结论,比如说 “超人速度的存在可能性”,那么这个结论在逻辑上是有效的,即使我们不知道 “速度先生” 究竟是谁。
Example: Prove that
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2Fff00c6c6-f372-48e6-b992-8901dc4201fd%2FUntitled.png?table=block&id=34dcbebd-6fc9-4d65-ad29-1b3b0384fa93&t=34dcbebd-6fc9-4d65-ad29-1b3b0384fa93&width=288&cache=v2)
Example: Prove that
![notion image](https://www.notion.so/image/https%3A%2F%2Fprod-files-secure.s3.us-west-2.amazonaws.com%2F08a0bace-dc95-4c44-98ba-bf2645496c46%2Fddbad66f-1507-4654-be96-aab322813602%2FUntitled.png?table=block&id=0b9b5f5a-da80-4d96-8724-8bc410dd5b8e&t=0b9b5f5a-da80-4d96-8724-8bc410dd5b8e&width=384&cache=v2)
- 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.