Existential instantiation
| Type | Rule of inference |
|---|---|
| Field | Predicate logic |
| Symbolic statement | {\displaystyle \exists xP\left({x}\right)\implies P\left({a}\right)} |
In predicate logic, existential instantiation (also called existential elimination)[1] [2] is a rule of inference which says that, given a formula of the form {\displaystyle (\exists x)\phi (x)}, one may infer {\displaystyle \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 {\displaystyle x} which is bound to {\displaystyle \exists x} must be uniformly replaced by c. This is implied by the notation {\displaystyle P\left({a}\right)}, but its explicit statement is often left out of explanations.
In one formal notation, the rule may be denoted by
- {\displaystyle \exists xP\left({x}\right)\implies P\left({a}\right)}
where a is a new constant symbol that has not appeared in the proof.
See also
[edit ]References
[edit ]- ^ Hurley, Patrick. A Concise Introduction to Logic (11th ed.). Wadsworth Pub Co, 2008. Pg. 454. ISBN 978-0-8400-3417-5
- ^ Copi, Irving M.; Cohen, Carl (2002). Introduction to logic (11th ed.). Upper Saddle River, N.J.: Prentice Hall. ISBN 978-0-13-033737-5.
