Existential instantiation
Transformation rules |
---|
Propositional calculus |
Rules of inference |
Rules of replacement |
Predicate logic |
In predicate logic, existential instantiation (also called existential elimination)[1][2][3] is a valid rule of inference which says that, given a formula of the form , one may infer
for a new constant or variable symbol c. The rule has the restriction that the constant or variable c introduced by the rule must be a new term that has not occurred earlier in the proof.
In one formal notation, the rule may be denoted
where a is an arbitrary term that has not been a part of our proof thus far.
See also
References
This article is issued from Wikipedia - version of the 12/11/2014. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.