In
predicate logic
First-order logic, also called predicate logic, predicate calculus, or quantificational logic, is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantified variables ove ...
, existential instantiation (also called existential elimination)
is a
rule of inference
Rules of inference are ways of deriving conclusions from premises. They are integral parts of formal logic, serving as norms of the Logical form, logical structure of Validity (logic), valid arguments. If an argument with true premises follows a ...
which says that, given a formula of the form
, one may infer
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
which is bound to
must be uniformly replaced by ''c''. This is implied by the notation
, 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.
See also
*
Existential fallacy
The existential fallacy, or existential instantiation, is a formal fallacy. In the existential fallacy, one presupposes that a class has members when one is not supposed to do so; i.e., when one should not assume existential import. Not to be c ...
*
Universal instantiation
In predicate logic, universal instantiation (UI; also called universal specification or universal elimination, and sometimes confused with '' dictum de omni'') is a valid rule of inference from a truth about each member of a class of individual ...
*
List of rules of inference
References
Rules of inference
Predicate logic
{{logic-stub