Existential quantification
= Existential quantification
{title2=$\exists x\,\varphi$}
{wiki}
<Existential quantification> forms $\exists x\,\varphi(x,\mathbf y)$. In a <first-order structure>, it is true at an assignment to $\mathbf y$ when some domain element makes the instance true. In <natural deduction>, elimination uses a fresh variable for the hypothetical witness; that variable may not escape into the conclusion or the remaining undischarged assumptions.