全称特化
| 全称特化 | |
|---|---|
| 术语名称 | 全称特化 |
| 英语名称 | universal instantiation |
| 别名 | 全称实例化, universal specialization, US, UI |
全称特化(universal instantiation / universal specialization, 缩写 UI / US)是谓词逻辑中的定理， 指一个全称命题可以推出去除其中量化表达式并将约束变元代入为任意项的命题， 也作为谓词公式间的基本推理规则。
这一规则将一个全称命题特化到一个实例，即针对某个项的命题上，因此称为全称特化。
定理
指永真式 [math]\displaystyle{ \vDash \forall x \varphi \rightarrow \varphi[t/x] }[/math] 。
意义
- 在自然演绎系统中，是一个推理规则：
- 全称特化： [math]\displaystyle{ \forall x\varphi \vdash \varphi[t/x] }[/math]
- 在 Hilbert 系统中，全称特化是公理。