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 ( ∃ ∃ --> x ) ϕ ϕ --> ( x ) {\displaystyle (\exists x)\phi (x)} , one may infer ϕ ϕ --> ( c ) {\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 x {\displaystyle x} which is bound to ∃ ∃ --> x {\displaystyle \exists x} must be uniformly replaced by c. This is implied by the notation P ( a ) {\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
where a is a new constant symbol that has not appeared in the proof.
This logic-related article is a stub. You can help Wikipedia by expanding it.
Lokasi Pengunjung: 3.144.15.7