# 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.