Existential elimination

In symbolic logic, a valid inference in a system of quantifier rules. An existential claim is“eliminated” by way of a subproof that assumes a name for the claim in question, provided that the name is not already in use. For example, if the claim is “Some dogs are playful,” ∃x(Dog(x) ^ Playful(x)), the assumptive name could be “Walter,” with the resulting assumptive sentence, Dog(walter) ^ Playful(walter). The ensuing subproof involves the derivation of the statement S, which closes the subproof. The statement S has then been proved from that existential quantifier elimination.