---
tag: WKPW4BAVQT
kind: concept
name: Existential instantiation
aliases: [existential-elimination]
sources:
  - wikipedia: en:34632680@r1308491839
    locator: Existential instantiation
    note: adopted
    mention: wikipedia://en/34632680
    sections: [Summary]
same_as:
  wikidata: Q2013340
  wikipedia: Existential instantiation
inventory: [AA2EYHXFS5]
---

## Summary

In predicate logic, **existential instantiation** (also called **existential elimination**) is a rule of inference which says that, given a formula of the form $(\exists x) \phi(x)$, one may infer $\phi(c)$ 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 $x$ which is bound to $\exists x$ must be uniformly replaced by *c*. This is implied by the notation $P\left({a}\right)$, but its explicit statement is often left out of explanations.