The complementary ∃Elim rule corresponds to giving a (new) name to a witness. Thus if you know "there exists some prime bigger than 5", then by ∃Elim we can think of giving some witness the
name (say) *c*, and end up concluding "*c* is a prime bigger than 5". The caveats are that *c* must be a new name not already used in the proof, and different from any
variables free in the conclusion we're aiming for. However, we will be able to use that variable *c* along with universal formulas to get useful statements.

Thus the general form of the rule is that . That is, we can rewrite the body of the exists, replacing the quantified variable *p* with any new variable name *c*,
subject to the restrictions just mentioned.

- 1146 reads