No More Posts Available.
No more pages to load.
In predicate logic, existential instantiation (also called existential elimination) 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
∃
x
P
(
x
)
⟹
P
(
a
)
{\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.
