存在推广

存在推广
术语名称	存在推广
英语名称	existential generalization
别名	EG

存在推广(existential generalization, 缩写 EG)是谓词逻辑中的定理， 指一个存在命题可以通过去除其中量化表达式并将约束变元代入为任意项的命题推出， 也作为谓词公式间的基本推理规则。

这一规则将一个具体的针对某个项的命题推广到一般变项的一个存在命题上，因此称为存在推广。

定理

指永真式 [math]\displaystyle{ \vDash \varphi[t/x]\rightarrow \exists x \varphi }[/math] 。

意义

• 在自然演绎系统中，是一个推理规则：
  • 存在推广： [math]\displaystyle{ \varphi(t/x) \vdash \exists x \varphi }[/math] 。
• 在 Hilbert 系统中，一般取全称量词作为基础符号，此时存在推广是一个定理。