全称实例化与存在泛化规则
概述
全称实例化与存在泛化规则（Universal Instantiation and Existential Generalization）：全称实例化（UI）允许从全称命题 推出任一个体的实例 ；存在泛化（EG）允许从个体实例 推出存在命题 。这两个规则是谓词逻辑中最基本、最常用的量词推理规则。
定理陈述
形式化陈述
定理（全称实例化规则 UI）：设 为一个全称命题， 为论域中任意一个体的名称（常项），则
定理（存在泛化规则 EG）：设 为论域中某个个体的名称， 为关于该个体的命题，则
其中：
- ：对论域中所有 ， 为真
- ：论域中存在某个 使得 为真
- ：特定个体 满足性质
各项说明：
- UI 中的 可以是论域中的任意个体——因为全称命题对所有个体都成立
- EG 中的 是论域中的某个个体——只要有一个个体满足性质，存在命题就成立
- UI 和 EG 的组合使用可以实现量词的”消除”和”引入”，是谓词逻辑证明的基本操作
证明概要
证明思路（量词的语义定义直接推导）
核心思想
这两个规则的正确性直接来源于全称量词和存在量词的语义定义。
详细步骤
第一步：全称实例化（UI）的语义论证
的语义定义：在给定解释下，论域中的每一个个体 都满足 。
既然每一个个体都满足 ，那么特别地，个体 也满足 ，即 为真。
因此，从 可以推出 。
直觉类比：如果”所有学生都通过了考试”为真，那么特别地，“张三通过了考试”也为真（张三是学生中的一个个体）。
第二步：存在泛化（EG）的语义论证
的语义定义：在给定解释下，论域中至少存在一个个体 满足 。
已知 为真，即个体 满足 。既然至少有一个个体（即 ）满足 ，那么 为真。
因此，从 可以推出 。
直觉类比：如果”张三通过了考试”为真，那么”有人通过了考试”自然也为真。
第三步：使用限制
- UI 的限制： 必须是论域中确定的个体名称，不能是自由变项。在形式证明中，UI 通常用于将全称命题转化为关于特定个体的命题，以便进一步推理。
- EG 的限制： 不能是被”临时假设”引入的个体名称（如存在实例化 EI 中引入的名称），除非该名称出现在论证的某个非假设性前提中。这一限制防止了从假设性实例错误地推出存在命题。
关键推论
- 推论1（UI + EG 的组合应用）：通过 UI 将全称命题实例化，进行推理后，再用 EG 将结果泛化为存在命题。这是谓词逻辑证明中最常见的量词处理模式。
- 推论2（与存在实例化的对称性）：存在实例化（EI）规则 （其中 是新名称）与 UI 形成对称：UI 从”所有”到”某个”，EI 从”存在”到”某个（新的）”。
- 推论3（全称泛化规则 UG）：UI 的逆操作是全称泛化（UG）：如果能够证明 对任意个体 都成立（即 是完全任意的，不依赖于任何关于 的特殊假设），则可以推出 。
应用场景
- 数学证明：在数学推理中，UI 对应于”任取一个元素”的操作，EG 对应于”存在性证明”的结论步骤。例如，证明”存在无理数 、 使得 是有理数”时，最后一步就是 EG。
- 谓词逻辑形式证明：在 自然演绎 系统中，UI 和 EG 是处理量词的基本规则，几乎所有涉及量词的证明都需要使用它们。
- 数据库查询：在关系数据库中，SQL 的
SELECT ... WHERE ...查询对应 UI（从全称约束中选取特定记录），EXISTS子查询对应 EG。 - 程序验证：在程序正确性证明中，循环不变式（“对所有迭代步都成立”）通过 UI 实例化为特定步的断言，存在性断言（“存在满足条件的变量值”）通过 EG 引入。