| 存在限定规则 rule of existential instantiation;rule of existential specification 某些自然演绎系统中的初始推演规则。一般记作ES。这一规则规定：如果公式S这样得自公式R：把R中的变项v的每一自由出现都代之以该演绎中先前没有用过的歧义名称，那么S就是可从(∃v)R推出的。这里要求歧义名称不得是先前用过的。所谓歧义名称是指一个不确定的，可以命名的个体的专名。引进歧义名称是为了用一个不确定的常项去代替存在量词。例如：据ES规则，则可从“(∃x)H(x)”推得H(a)，其中a为歧义名称。存在限定规则在有些逻辑公理系统中，也作为导出公理出现。 |