Existential quantification
Rules of inference

A rule of inference is a rule justifying a logical step from hypothesis to conclusion. There are several rules of inference which utilize the existential quantifier.

Existential introduction (∃I) concludes that, if the propositional function is known to be true for a particular element of the domain of discourse, then it must be true that there exists an element for which the proposition function is true. Symbolically,

Existential instantiation, when conducted in a Fitch style deduction, proceeds by entering a new sub-derivation while substituting an existentially quantified variable for a subject—which does not appear within any active sub-derivation. If a conclusion can be reached within this sub-derivation in which the substituted subject does not appear, then one can exit that sub-derivation with that conclusion. The reasoning behind existential elimination (∃E) is as follows: If it is given that there exists an element for which the proposition function is true, and if a conclusion can be reached by giving that element an arbitrary name, that conclusion is necessarily true, as long as it does not contain the name. Symbolically, for an arbitrary c and for a proposition Q in which c does not appear:

P (c) → Q {\displaystyle P(c)\to \ Q} must be true for all values of c over the same domain X; else, the logic does not follow: If c is not arbitrary, and is instead a specific element of the domain of discourse, then stating P (c) might unjustifiably give more information about that object.
combination:two_responses