Loading AI tools
From Wikipedia, the free encyclopedia
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 , 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.
Type | Rule of inference |
---|---|
Field | Predicate logic |
Symbolic statement |
In one formal notation, the rule may be denoted by
where a is a new constant symbol that has not appeared in the proof.
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.