Existential instantiation

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 (\exists x) \phi(x), one may infer \phi(c) 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

(\exists x)\mathcal{F}x :: \mathcal{F}a ,

where a is an arbitrary term that has not been a part of our proof thus far.

See also

References

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