# Existential instantiation

Type | Rule of inference |
---|---|

Field | Predicate logic |

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 rule of inference which says that, given a formula of the form [math]\displaystyle{ (\exists x) \phi(x) }[/math], one may infer [math]\displaystyle{ \phi(c) }[/math] for a new constant symbol *c*. The rule has the restrictions that the constant *c* introduced by the rule must be a new term that has not occurred earlier in the proof, and it also must not occur in the conclusion of the proof. It is also necessary that every instance of [math]\displaystyle{ x }[/math] which is bound to [math]\displaystyle{ \exists x }[/math] must be uniformly replaced by *c*. This is implied by the notation [math]\displaystyle{ P\left({a}\right) }[/math], but its explicit statement is often left out of explanations.

In one formal notation, the rule may be denoted by

- [math]\displaystyle{ \exists x P \left({x}\right) \implies P \left({a}\right) }[/math]

where *a* is a new constant symbol that has not appeared in the proof.

## See also

## References

Original source: https://en.wikipedia.org/wiki/Existential instantiation.
Read more |