Exists-Elim

Available under Creative Commons-ShareAlike 4.0 International License. Download for free at http://cnx.org/contents/383d4b87-2d7b-454e-99fe-2eaa43eae8ff@20.20

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.