= Existential quantification over a finitely named domain
{title2=$\exists x\,Q(x)\ \longleftrightarrow\ Q(c_1)\lor\cdots\lor Q(c_n)$}
Assume $\forall x\,(x=c_1\lor\cdots\lor x=c_n)$ with $n\ge1$. For the forward implication, open a fresh existential witness, instantiate domain exhaustiveness at it, and split into the equality cases. The <equality elimination rule> transfers its predicate to the corresponding constant, which supplies the required disjunct. Closing the witness scope is legal because the result contains only the named constants. Conversely each named instance gives the existential by the <existential quantifier introduction rule>, and cases combine those derivations. The constants need not denote distinct objects. A negated named instance can eliminate one case through contradiction and <logical falsity elimination rule>.
Back to article page
