Existential instantiation | |
Type: | Rule of inference |
Field: | Predicate logic |
Symbolic Statement: | \existsxP\left({x}\right)\impliesP\left({a}\right) |
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
(\existsx)\phi(x)
\phi(c)
x
\existsx
P\left({a}\right)
In one formal notation, the rule may be denoted by
\existsxP\left({x}\right)\impliesP\left({a}\right)