Existential instantiation explained

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)

, 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

\existsx

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.

In one formal notation, the rule may be denoted by

\existsxP\left({x}\right)\impliesP\left({a}\right)

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

See also

Notes and References

  1. Hurley, Patrick. A Concise Introduction to Logic. Wadsworth Pub Co, 2008.
  2. Copi and Cohen
  3. Moore and Parker